leo@(this domain)
On the summit of Snowfield Peak, July 4, 2015.  Photograph by Bing Gao.


PhD, Pure Mathematics. 2008
MA, Mathematics. 2003
University of California, Los Angeles
Thesis supervisor: William Duke
Fourier Coefficients of Triangle Functions
MS, Computer Science and Engineering. 1990
BS, Electrical Engineering and Computer Science. 1990
BS, Mathematics. 1990
Massachusetts Institute of Technology
MS Thesis supervisor: Nancy Lynch
Dynamic process creation in a static model

Professional Experience

Halfaya Research. 2017 to present
Bellevue, WA
Independent Researcher
Maana, Inc. 2015—2017
Bellevue, WA
Senior Software Engineer
Amazon Web Services, Inc. 2013—2015
Seattle, WA
Software Development Engineer
Expedia, Inc. 2011—2013
Bellevue, WA
Senior Software Engineer
Castilleja School. 2008—2011
Palo Alto, CA
Mathematics Faculty
Siebel Systems, Inc. 1997—2002
San Mateo, CA
Senior Software Engineer
Oracle Corporation. 1994—1997
Redwood Shores, CA
Senior Technical Staff
Matsushita Communication Industrial. 1991—1993
Yokohama, Japan
Technical Staff


Adapting Proof Automation to Adapt Proofs
Talia Ringer, Nathaniel Yazdani, John Leo, and Dan Grossman
Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP’18)
See also Pumpkin Patch


Dependent Types in GHC
BayHac 2017, April 8, 2017


Method and device for processing a time related data entry. 2010
Jasjeet Singh Thind, John Leo, Yoram Tal and Maria Kaval
United States Patent Number 7,711,855
Parallel distinct aggregates. 2002
John Leo, Cetin Ozbutun, Bill Waddington and Shivani Gupta
United States Patent Number 6,430,550

See also my LinkedIn page.

Additional experience, older publications, etc, omitted. Contact me for a detailed CV.