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.

Research

I study the syntax and semantics of type theory and programming languages, through an algebraic lens. I am particularly interested in the semantics of syntax, applying categorical techniques such as gluing to obtain abstract normalization results. My colleagues and I are developing the redtt proof assistant for Cartesian cubical type theory.

Some of my collaborators include Carlo Angiuli, Lars Birkedal, Evan Cavallo, David Thrane Christiansen, Favonia, Daniel Gratzer, Robert Harper, Darin Morrison, and Anders Mörtberg.

Publications

J. Sterling, C. Angiuli, and D. Gratzer Cubical Syntax for Reflection-Free Extensional Equality (To Appear) International Conference on Formal Structures for Computation and Deduction (FSCD), 2019
Extended Version, Citation
C. Angiuli, E. Cavallo, K. Hou (Favonia), R. Harper, and J. Sterling The RedPRL Proof Assistant (Invited Paper) International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP), 2018
Citation
J. Sterling, R. Harper Guarded Computational Type Theory Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS '18)
Short Version, Extended Version, Citation
D. McAdams, J. Sterling Dependent Types for Pragmatics 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.
Citation

Selected Talks

C. Angiuli, E. Cavallo, Favonia, R. Harper, A. Mőrtberg and J. Sterling redtt: implementing cartesian cubical type theory Dagstuhl Seminar 18341: Formalization of Mathematics in Type Theory
J. Sterling, R. Harper Guarded Computational Type Theory Logic in Computer Science (LICS '18)
J. Sterling Forcing Bar Induction in System T Logic Colloquium, Indiana University, August 2016

Preprints

D. Gratzer, J. Sterling, and L. Birkedal Implementing Modal Dependent Type Theory March 2019
Technical Report, Implementation
J. Sterling Algebraic Type Theory and Universe Hierarchies December 2018
J. Sterling, B. Spitters Normalization by gluing for free λ-theories August 2018
J. Sterling, R. Harper Algebraic Foundations of Proof Refinement Winter 2017
J. Sterling Forcing Bar Induction in System T Fall 2016

Lectures and Tutorials

Algebraic Type Theory and the Gluing Construction April 2019 Lecture for the CMU HoTT Seminar
Substructural Deduction Fall 2017 Guest lecture for Constructive Logic (15-317)
Implementing Inference Rules in Standard ML Fall 2017 Tutorial for Constructive Logic (15-317)
Grothendieck Toposes Spring 2017 Guest lecture for Categorical Logic (80-514-814)

Teaching

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

Awards and Honors

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