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; currently, I am interested in models and implementation of higher dimensional and modal 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 modal dependent type theory.

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

Publications and 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)
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)

Preprints

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)
Remark on the Hypothetical Judgment.
Fall 2015.
(PDF)

Teaching

Fall 2018: TA for Constructive Logic (15-317) with Karl Crary.
Fall 2017: TA for Constructive Logic (15-317) with Frank Pfenning.

Lecture Notes, Tutorials

Substructural Deduction. Fall 2017. Guest lecture for Constructive Logic (15-317).
Implementing Inference Rules in Standard ML . Fall 2017.
Grothendieck Toposes. Spring 2017. Guest lecture for Categorical Logic (80-514-814).

Other Activities

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