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

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, C. Angiuli and D. Gratzer Cubical Syntax for Reflection-Free Extensional Equality February 2019
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

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.