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 have developed the redtt proof assistant for Cartesian cubical type theory.

Publications

D. Gratzer, J. Sterling, and L. Birkedal. Implementing a Modal Dependent Type Theory. International Conference on Functional Programming (ICFP), 2019. Distinguished Paper Award.
Preprint, Technical Report, Implementation, Citation
J. Sterling, C. Angiuli, and D. Gratzer. Cubical Syntax for Reflection-Free Extensional Equality. International Conference on Formal Structures for Computation and Deduction (FSCD), 2019. Best Paper Award For Junior Researchers.
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

J. Sterling, C. Angiuli, and D. Gratzer. Cubical Exact Equality and Categorical Gluing. International Conference on Homotopy Type Theory, 2019.
J. Sterling, C. Angiuli, and D. Gratzer. Cubical Syntax for Reflection-Free Extensional Equality. International Conference on Formal Structures for Computation and Deduction (FSCD), 2019.
J. Sterling, C. Angiuli, and D. Gratzer. XTT: Cubical Syntax for Extensional Equality (without equality reflection). TYPES, 2019.
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 and 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

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.

Selected Lectures

Sharpen the Abstract to Firmly Grasp the Concrete! May 2019. Guest lecture for Computational Higher Type Theory (15-819)
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

(2019) ICFP 2019 Distinguished Paper Award
(2019) FSCD 2019 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.