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 of higher dimensional type theory as well as guarded dependent type theory. My colleagues and I have developed the RedPRL proof assistant 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.

Teaching

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

Publications

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

Preprints

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

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