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 have developed the
redtt proof assistant
for Cartesian cubical type theory.
Recent News

July 2019: Implementing a Modal Dependent Type Theory receives ICFP 2019 Distinguished Paper Award.

June 2019: Cubical Syntax for ReflectionFree Extensional Equality receives FSCD 2019 Best Paper Award for Junior Researchers.

June 2019: Implementing a Modal Dependent Type Theory accepted at ICFP 2019.

April 2019: Cubical Syntax for ReflectionFree Extensional Equality accepted at FSCD 2019.
Publications

D. Gratzer, J. Sterling, and L. Birkedal.
Implementing a Modal Dependent Type Theory.
International Conference on Functional Programming (ICFP), 2019.
Distinguished Paper Award.

J. Sterling, C. Angiuli, and D. Gratzer.
Cubical Syntax for ReflectionFree Extensional Equality.
International Conference on Formal Structures for Computation and Deduction (FSCD), 2019.
Best Paper Award For Junior Researchers.

C. Angiuli, E. Cavallo, K. Hou (Favonia), R. Harper, and J. Sterling.
The RedPRL Proof Assistant.
(Invited Paper)
International Workshop on Logical Frameworks and MetaLanguages: 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

J. Sterling, C. Angiuli, and D. Gratzer.
Cubical Exact Equality and Categorical Gluing.
International Conference on Homotopy Type Theory, 2019.

J. Sterling, C. Angiuli, and D. Gratzer.
Cubical Syntax for ReflectionFree Extensional Equality.
International Conference on Formal Structures for Computation and Deduction (FSCD), 2019.

J. Sterling, C. Angiuli, and D. Gratzer.
XTT: Cubical Syntax for Extensional Equality (without equality reflection).
TYPES, 2019.

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

J. Sterling and R. Harper.
Guarded Computational Type Theory.
Logic in Computer Science (LICS '18).

J. Sterling.
Forcing Bar Induction in System T.
Logic Colloquium, Indiana University, August 2016.
Awards and Honors

(2019) ICFP 2019 Distinguished Paper Award

(2019) FSCD 2019 Best Paper Award for Junior Researchers

(2011) W.K. Pritchett Prize in Elementary Greek, UC Berkeley
Other Activities
Together with my cohosts David Christiansen and Darin Morrison, I helped
create The Type Theory
Podcast.