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, ancient languages and literature, Marxism-Leninism-Maoism and Mao Zedong Thought.

Research Projects

• CTT_🕒: computational models of guarded dependent type theory.
• RedPRL: implementing Computational Higher-Dimensional Type Theory.
• RedML: theory and practice of proof metalanguages.

Teaching

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

Publications

• J. Sterling and R. Harper. Guarded Computational Type Theory. Logic in Computer Science (LICS), 2018. (Short PDF, Long PDF)

Preprints

• J. Sterling and R. Harper. Algebraic Foundations of Proof Refinement. Winter 2017. (PDF)
• J. Sterling. Forcing Bar Induction in System T. Fall 2016. (PDF)
• J. Sterling. 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