Jon Sterling

I am a doctoral student of Robert Harper at Carnegie Mellon University studying type theory, programming languages and semantics. Previously I received a B.A. in Linguistics from U.C. Berkeley. My other interests include category theory, topos theory, formalization of mathematics, Assyriology, and ancient languages and literature. Check out my new research blog! Access my curriculum vitae

Research

I study the syntax and semantics of type theory and programming languages through the lens of categorical algebra and topos theory, with an aim toward building better interactive proof assistants. I am interested in the design and metatheory of program module calculi as in ML family languages.

My colleagues and I have developed the redtt and cooltt proof assistants for Cartesian cubical type theory.

Recent News

Aug. 2020	thesis proposal presented and accepted
Jul. 2019	received ICFP '19 Distinguished Paper Award
Jun. 2019	received FSCD '19 Best Paper Award for Junior Researchers

Recent Drafts

Jun. 2021	Abstract A metalanguage for multi-phase modularity J. Sterling, R. Harper latest version
Dec. 2020	Preprint Syntactic categories for dependent type theory: sketching and adequacy D. Gratzer, J. Sterling arXiv preprint, latest version
Feb. 2020	Preprint A Cubical Language for Bishop Sets J. Sterling, C. Angiuli, and D. Gratzer arXiv preprint latest version (revised May 2021)

Publications

JACM	To appear Logical Relations as Types: Proof-Relevant Parametricity for Program Modules Journal of the ACM (accepted pending minor revision) J. Sterling, R. Harper arXiv preprint, latest version (revised May 2021)
LICS '21	To appear Normalization for Cubical Type Theory 36th Annual Symposium on Logic in Computer Science J. Sterling, C. Angiuli arXiv preprint, latest version, citation, video, slides
JFP	Higher order functions and Brouwer's Thesis Journal of Functional Programming, Bob Harper Festschrift Collection CambridgeCore, arXiv preprint, Agda formalization, citation
ICFP '19	Implementing a Modal Dependent Type Theory D. Gratzer, J. Sterling, and L. Birkedal International Conference on Functional Programming (ICFP), 2019 Distinguished Paper Award ACM DL, preprint, technical report, implementation, citation
FSCD '19	Cubical Syntax for Reflection-Free Extensional Equality J. Sterling, C. Angiuli, and D. Gratzer International Conference on Formal Structures for Computation and Deduction (FSCD), 2019 Best Paper Award For Junior Researchers DROPS, extended version (arXiv), slides, citation
LFMTP '18	The RedPRL Proof Assistant C. Angiuli, E. Cavallo, K. Hou (Favonia), R. Harper, and J. Sterling International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP), 2018 Invited Paper EPTCS, citation
LICS '18	Guarded Computational Type Theory J. Sterling, R. Harper Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS '18) ACM DL, short preprint, long preprint (arXiv), slides, citation
Apr. 2016	Dependent Types for Pragmatics D. McAdams, J. Sterling Redmond J., Pombo Martins O., Nepomuceno Fernández Á. (eds) Epistemology, Knowledge and the Impact of Interaction. Logic, Epistemology, and the Unity of Science, vol 38. Springer, Cham. SpringerLink, citation

Selected Talks

(Conference talks listed with publications.)

May 2021	Normalization for Cubical Type Theory Padova Logic Seminar
Apr. 2021	Logical Relations As Types CCS Colloquium, Augusta University. Slides, Video
Feb. 2021	Normalization for Cubical Type Theory Pittsburgh's HoTT Seminar
Aug. 2020	Objective Metatheory of (Cubical) Type Theories Thesis Proposal
Jun. 2020	redtt and the future of Cartesian cubical type theory Every Proof Assistant Video
Mar. 2020	Objective Metatheory of Dependent Type Theories HoTTEST Slides, Video
Mar. 2020	(Cubical) Computability Structures MURI Grant Meeting
Jan. 2020	Gluing Models of Type Theory Along Flat Functors J. Sterling and C. Angiuli CMU HoTT Seminar
HoTT '19	Cubical Exact Equality and Categorical Gluing J. Sterling, C. Angiuli, and D. Gratzer International Conference on Homotopy Type Theory, 2019
TYPES '19	XTT: Cubical Syntax for Extensional Equality (without equality reflection) J. Sterling, C. Angiuli, and D. Gratzer TYPES, 2019
Apr. 2019	Algebraic Type Theory and the Gluing Construction CMU HoTT Seminar
Aug. 2018	redtt: implementing cartesian cubical type theory C. Angiuli, E. Cavallo, Favonia, R. Harper, A. Mőrtberg, and J. Sterling Dagstuhl Seminar 18341: Formalization of Mathematics in Type Theory

Lectures and Research Notes

Oct. 2020	Notes A Synthetic Realignment Theorem latest version
Apr. 2020	Notes An OK Version of Type Theory latest version
Feb. 2020	Notes Connectives in Semantics of Type Theory latest version
Fall 2017	Lecture Substructural Deduction Guest lecture for Constructive Logic (15-317) at CMU lecture notes
Fall 2017	Lecture Implementing Inference Rules in Standard ML Tutorial for Constructive Logic (15-317) as CMU lecture notes

Teaching

Fall 2018	TA for Constructive Logic (15-317) with Karl Crary
Fall 2017	TA for Constructive Logic (15-317) with Frank Pfenning

Academic Service

I have served as an external reviewer or subreviewer for CSL (2021), ESOP (2021), FSCD (2019, 2020), FoSSaCS (2021), LICS (2017, 2021); and as a referee for LMCS and MSCS.

I am a mentor for the SIGPLAN long-term mentoring program for programming languges researchers (SIGPLAN-M).

Awards and Honors

2019	ICFP '19 Distinguished Paper Award
2019	FSCD '19 Best Paper Award for Junior Researchers
2011	W.K. Pritchett Prize in Elementary Greek, UC Berkeley

Other Activities

Together with my co-hosts David Christiansen and Darin Morrison, I helped create The Type Theory Podcast.