Education

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

Google. 2018 to 2020

Seattle, WA
Software Engineer

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

Publications

Proof Repair across Type Equivalences

Talia Ringer, RanDair Porter, Nathaniel Yazdani, John Leo, and Dan Grossman
PLDI 2021: Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation

Ornaments for Proof Reuse in Coq

Talia Ringer, Nathaniel Yazdani, John Leo, and Dan Grossman
ITP 2019: Interactive Theorem Proving

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

Presentations

Counterpoint by Construction

Youyou Cong and John Leo
The 7th ACM SIGPLAN Workshop on Functional Art, Music, Modelling and Design (FARM 2019), Berlin, Germany, August 2019
slides
video

Musical Ornaments (starts at 34:55)

Workshop on Programming Languages and Software Engineering Research in the Pacific Northwest, May 14, 2018

Dependent Types in GHC

BayHac 2017, April 8, 2017

Patents

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.