Jon Sterling

9225 Gates Hilman Center
School of Computer Science
Carnegie Mellon University
5000 Forbes Ave
Pittsburgh, PA 15213
j...@cs.cmu.edu

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
  • 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

Preprints

Lectures and Tutorials

Teaching

Awards and Honors

Other Activities

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