Jon Sterling

9225 Gates Hillman Center
School of Computer Science
Carnegie Mellon University
5000 Forbes Ave
Pittsburgh, PA 15213

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.


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.


  • D. Gratzer, J. Sterling, and L. Birkedal. Implementing Modal Dependent Type Theory. (Conditionally Accepted) International Conference on Functional Programming (ICFP), 2019.
  • 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.
  • 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.
  • J. Sterling, R. Harper. Guarded Computational Type Theory. Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS '18).
  • 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.

Selected Talks


Selected Lectures


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.