CV

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. 20182020

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

Talk and demonstration at the Joint Mathematics Meetings in San Francisco, January 3, 2024.
Slides. Music Video

Counterpoint Analysis and Synthesis

Agda Implementors' Meeting XXXI, Edinburgh, Scotland, November 2022

Demo: Counterpoint Analysis and Synthesis

The 10th ACM SIGPLAN Workshop on Functional Art, Music, Modelling and Design (FARM 2022), Ljubljana, Slovenia, September 2022
video

Performance: Logical Soundness

The 9th ACM SIGPLAN Workshop on Functional Art, Music, Modelling and Design (FARM 2021), Online, August 2021
video full session

Demo: 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

Renzoku Ren'ai Dorama

First Conference on Japanese Popular Culture, University of Victoria, British Columbia, Canada, April 12, 1997.

Service

Association for Computing Machinery

Club Northwest


Seattle Mountaineers

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

Additional experience, older publications, etc, omitted.