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

  • The RedPRL Proof Assistant (Invited Paper).
    C. Angiuli, E. Cavallo, Favonia, R. Harper and J. Sterling.
    LFMTP, 2018.
    (PDF)
  • Guarded Computational Type Theory.
    J. Sterling and R. Harper.
    Logic in Computer Science (LICS), 2018.
    (Short PDF, Long PDF, Slides)

Talks

  • redtt: implementing cartesian cubical type theory.
    C. Angiuli, E. Cavallo, Favonia, R. Harper, A. Mőrtberg and J. Sterling.
    Dagstuhl Seminar 18341: Formalization of Mathematics in Type Theory
    (Slides)

Preprints

  • Implementing Modal Dependent Type Theory.
    D. Gratzer, J. Sterling and L. Birkedal
    March 2019
    (Short PDF, Technical Report, Implementation)
  • Cubical Syntax for Reflection-Free Extensional Equality.
    J. Sterling, C. Angiuli and D. Gratzer.
    February 2019.
    (PDF)
  • Algebraic Type Theory and Universe Hierarchies.
    December 2018.
    (PDF)
  • Normalization by gluing for free λ-theories.
    J. Sterling and B. Spitters.
    August 2018.
    (PDF)
  • Algebraic Foundations of Proof Refinement.
    J. Sterling and R. Harper.
    Winter 2017.
    (PDF)
  • Forcing Bar Induction in System T.
    Fall 2016.
    (PDF)

Teaching

Lecture Notes, Tutorials

Other Activities

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