Jon Sterling

9225 Gates Hilman 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; currently, I am interested in models of higher dimensional type theory as well as guarded dependent type theory. My colleagues and I are developing the RedPRL and redtt proof assistants for cartesian cubical type theory. Today, I am studying definitional equivalence, normal forms and type checking for cartesian cubical type theory and guarded dependent type theory.

My collaborators include (in no particular order) Carlo Angiuli, Lars Birkedal, Evan Cavallo, David Thrane Christiansen, Ranald Clouston, Favonia, Daniel Gratzer, Robert Harper, Darin Morrison, Anders Mörtberg, and Bas Spitters.




Lecture Notes, Tutorials

Other Activities

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