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. 2018—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
Talk and demonstration at the Joint Mathematics Meetings in San Francisco, Wednesday, January 3, 3:00-3:30pm.
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
BayHac 2017, April 8, 2017
First Conference on Japanese Popular Culture, University of Victoria, British Columbia, Canada, April 12, 1997.
Service
Association for Computing Machinery
General Chair (2022) and Program Chair (2023) of the ACM SIGPLAN Workshop on Functional Art, Music, Modelling and Design (FARM)
Member of the Artifact Evaluation Committee (AEC) for the ACM SIGPLAN International Conference on Functional Programming (ICFP): 2021, 2022 and 2023
SIGPLAN-M mentor: 2020—2022
Club Northwest
Vice President of Teams and member of the Board of Directors: 2020—2023
Seattle Mountaineers
Alpine Climb Leader (2014—2019)
Alpine Scramble Leader (2013—2019)
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.