Dependent Types for Pragmatics. - Darryl McAdams; Jonathan Sterling (CoRR, 2014)

Remark on the hypothetical judgment. - Jonathan Sterling (CoRR, 2015)

Type Theory and its Meaning Explanations. - Jonathan Sterling (CoRR, 2015)

Primitive Recursive Bars Are Inductive. - Jonathan Sterling (CoRR, 2016)

Syntax and Semantics of Abstract Binding Trees. - Jonathan Sterling; Darin Morrison (CoRR, 2016)

Algebraic Foundations of Proof Refinement. - Jonathan Sterling; Robert Harper 001 (CoRR, 2017)

Guarded Computational Type Theory. - Jonathan Sterling; Robert Harper 001 (LICS, 2018)

The RedPRL Proof Assistant (Invited Paper). - Carlo Angiuli; Evan Cavallo; Kuen-Bang Hou (Favonia); Robert Harper 001; Jonathan Sterling (LFMTP@FSCD, 2018)

Normalization by gluing for free λ-theories. - Jonathan Sterling; Bas Spitters (CoRR, 2018)

Cubical Syntax for Reflection-Free Extensional Equality. - Jonathan Sterling; Carlo Angiuli; Daniel Gratzer (FSCD, 2019)

Algebraic Type Theory and Universe Hierarchies. - Jonathan Sterling (CoRR, 2019)

Implementing a modal dependent type theory. - Daniel Gratzer; Jonathan Sterling; Lars Birkedal (Proc. ACM Program. Lang., 2019)

Syntactic categories for dependent type theory: sketching and adequacy. - Daniel Gratzer; Jonathan Sterling (CoRR, 2020)

Normalization for Cubical Type Theory. - Jonathan Sterling; Carlo Angiuli (LICS, 2021)

Logical Relations as Types: Proof-Relevant Parametricity for Program Modules. - Jonathan Sterling; Robert Harper 001 (J. ACM, 2021)

Higher order functions and Brouwer's thesis. - Jonathan Sterling (J. Funct. Program., 2021)

Sheaf Semantics of Termination-Insensitive Noninterference. - Jonathan Sterling; Robert Harper 001 (FSCD, 2022)

The directed plump ordering. - Daniel Gratzer; Michael Shulman; Jonathan Sterling (CoRR, 2022)

Bilimits in categories of partial maps. - Jonathan Sterling (CoRR, 2022)

Strict universes for Grothendieck topoi. - Daniel Gratzer; Michael Shulman; Jonathan Sterling (CoRR, 2022)

Reflections on existential types. - Jonathan Sterling (CoRR, 2022)

Denotational semantics of general store and polymorphism. - Jonathan Sterling; Daniel Gratzer; Lars Birkedal (CoRR, 2022)

Classifying topoi in synthetic guarded domain theory. - Daniele Palombi; Jonathan Sterling (MFPS, 2022)

Controlling unfolding in type theory. - Daniel Gratzer; Jonathan Sterling; Carlo Angiuli; Thierry Coquand; Lars Birkedal (CoRR, 2022)

A Cubical Language for Bishop Sets. - Jonathan Sterling; Carlo Angiuli; Daniel Gratzer (Log. Methods Comput. Sci., 2022)

A cost-aware logical framework. - Yue Niu; Jonathan Sterling; Harrison Grodin; Robert Harper 001 (Proc. ACM Program. Lang., 2022)

First Steps in Synthetic Tait Computability: The Objective Metatheory of Cubical Type Theory. - Jonathan Sterling (2022)

Towards a geometry for syntax. - Jonathan Sterling (CoRR, 2023)

Free theorems from univalent reference types. - Jonathan Sterling; Daniel Gratzer; Lars Birkedal (CoRR, 2023)

A denotationally-based program logic for higher-order store. - Frederik Lerbjerg Aagaard; Jonathan Sterling; Lars Birkedal (MFPS, 2023)

Tensorial structure of the lifting doctrine in constructive domain theory. - Jonathan Sterling (CoRR, 2023)

What should a generic object be? - Jonathan Sterling (Math. Struct. Comput. Sci., 2023)

The Essence of Generalized Algebraic Data Types. - Filip Sieczkowski; Sergei Stepanenko; Jonathan Sterling; Lars Birkedal (Zenodo, 2023)

The Essence of Generalized Algebraic Data Types. - Filip Sieczkowski; Sergei Stepanenko; Jonathan Sterling; Lars Birkedal (Zenodo, 2023)

The Essence of Generalized Algebraic Data Types. - Filip Sieczkowski; Sergei Stepanenko; Jonathan Sterling; Lars Birkedal (Zenodo, 2023)

Towards Univalent Reference Types: The Impact of Univalence on Denotational Semantics. - Jonathan Sterling; Daniel Gratzer; Lars Birkedal (CSL, 2024)

Cost-sensitive computational adequacy of higher-order recursion in synthetic domain theory. - Yue Niu; Jonathan Sterling; Robert Harper 001 (CoRR, 2024)

Reflexive graph lenses in univalent foundations. - Jonathan Sterling (CoRR, 2024)

Decalf: A Directed, Effectful Cost-Aware Logical Framework. - Harrison Grodin; Yue Niu; Jonathan Sterling; Robert Harper 001 (Proc. ACM Program. Lang., 2024)

The Essence of Generalized Algebraic Data Types. - Filip Sieczkowski; Sergei Stepanenko; Jonathan Sterling; Lars Birkedal (Proc. ACM Program. Lang., 2024)

When is the partial map classifier a Sierpiński cone? - Leoni Pugh; Jonathan Sterling (CoRR, 2025)

Hofmann-Streicher lifting of fibred categories. - Andrew Slattery; Jonathan Sterling (CoRR, 2025)

Domains and Classifying Topoi. - Jonathan Sterling; Lingyuan Ye (CoRR, 2025)