Jonathan Sterling

Publication Activity (10 Years)

Years Active: 2014-2024
Publications (10 Years): 42

Top Topics

Logical Framework

Syntactic Categories

Denotational Semantics

Higher Order Logic

Top Venues

Proc. ACM Program. Lang.

Publications

Filip Sieczkowski, Sergei Stepanenko, Jonathan Sterling, Lars Birkedal
The Essence of Generalized Algebraic Data Types. Proc. ACM Program. Lang. 8 (POPL) (2024)
Jonathan Sterling
Reflexive graph lenses in univalent foundations. CoRR (2024)
Harrison Grodin, Yue Niu, Jonathan Sterling, Robert Harper
Decalf: A Directed, Effectful Cost-Aware Logical Framework. Proc. ACM Program. Lang. 8 (POPL) (2024)
Jonathan Sterling, Daniel Gratzer, Lars Birkedal
Towards Univalent Reference Types: The Impact of Univalence on Denotational Semantics. CSL (2024)
Yue Niu, Jonathan Sterling, Robert Harper
Cost-sensitive computational adequacy of higher-order recursion in synthetic domain theory. CoRR (2024)
Jonathan Sterling
Towards a geometry for syntax. CoRR (2023)
Jonathan Sterling
What should a generic object be? Math. Struct. Comput. Sci. 33 (1) (2023)
Frederik Lerbjerg Aagaard, Jonathan Sterling, Lars Birkedal
A denotationally-based program logic for higher-order store. CoRR (2023)
Harrison Grodin, Robert Harper, Yue Niu, Jonathan Sterling
Decalf: A Directed, Effectful Cost-Aware Logical Framework. CoRR (2023)
Jonathan Sterling
Tensorial structure of the lifting doctrine in constructive domain theory. CoRR (2023)
Jonathan Sterling, Daniel Gratzer, Lars Birkedal
Free theorems from univalent reference types. CoRR (2023)
Jonathan Sterling, Robert Harper
Sheaf semantics of termination-insensitive noninterference. CoRR (2022)
Daniele Palombi, Jonathan Sterling
Classifying topoi in synthetic guarded domain theory. CoRR (2022)
Jonathan Sterling, Carlo Angiuli, Daniel Gratzer
A Cubical Language for Bishop Sets. Log. Methods Comput. Sci. 18 (1) (2022)
Daniel Gratzer, Michael Shulman, Jonathan Sterling
Strict universes for Grothendieck topoi. CoRR (2022)
Jonathan Sterling, Daniel Gratzer, Lars Birkedal
Denotational semantics of general store and polymorphism. CoRR (2022)
Jonathan Sterling
Reflections on existential types. CoRR (2022)
Yue Niu, Jonathan Sterling, Harrison Grodin, Robert Harper
A cost-aware logical framework. Proc. ACM Program. Lang. 6 (POPL) (2022)
Daniel Gratzer, Michael Shulman, Jonathan Sterling
The directed plump ordering. CoRR (2022)
Jonathan Sterling
What should a generic object be? CoRR (2022)
Daniel Gratzer, Jonathan Sterling, Carlo Angiuli, Thierry Coquand, Lars Birkedal
Controlling unfolding in type theory. CoRR (2022)
Jonathan Sterling, Robert Harper
Sheaf Semantics of Termination-Insensitive Noninterference. FSCD (2022)
Jonathan Sterling
Bilimits in categories of partial maps. CoRR (2022)
Jonathan Sterling, Carlo Angiuli
Normalization for Cubical Type Theory. CoRR (2021)
Jonathan Sterling
Higher order functions and Brouwer's thesis. J. Funct. Program. 31 (2021)
Jonathan Sterling, Robert Harper
Logical Relations as Types: Proof-Relevant Parametricity for Program Modules. J. ACM 68 (6) (2021)
Jonathan Sterling, Carlo Angiuli
Normalization for Cubical Type Theory. LICS (2021)
Yue Niu, Jonathan Sterling, Harrison Grodin, Robert Harper
A cost-aware logical framework. CoRR (2021)
Jonathan Sterling, Carlo Angiuli, Daniel Gratzer
A Cubical Language for Bishop Sets. CoRR (2020)
Jonathan Sterling, Robert Harper
Logical Relations as Types: Proof-Relevant Parametricity for Program Modules. CoRR (2020)
Daniel Gratzer, Jonathan Sterling
Syntactic categories for dependent type theory: sketching and adequacy. CoRR (2020)
Jonathan Sterling, Carlo Angiuli, Daniel Gratzer
Cubical Syntax for Reflection-Free Extensional Equality. FSCD (2019)
Jonathan Sterling
Algebraic Type Theory and Universe Hierarchies. CoRR (2019)
Daniel Gratzer, Jonathan Sterling, Lars Birkedal
Implementing a modal dependent type theory. Proc. ACM Program. Lang. 3 (ICFP) (2019)
Jonathan Sterling, Carlo Angiuli, Daniel Gratzer
Cubical Syntax for Reflection-Free Extensional Equality. CoRR (2019)
Jonathan Sterling, Robert Harper
Guarded Computational Type Theory. CoRR (2018)
Jonathan Sterling, Bas Spitters
Normalization by gluing for free λ-theories. CoRR (2018)
Carlo Angiuli, Evan Cavallo, Kuen-Bang Hou, Robert Harper, Jonathan Sterling
The RedPRL Proof Assistant (Invited Paper). LFMTP@FSCD (2018)
Jonathan Sterling, Robert Harper
Guarded Computational Type Theory. LICS (2018)
Jonathan Sterling, Robert Harper
Algebraic Foundations of Proof Refinement. CoRR (2017)
Jonathan Sterling, Darin Morrison
Syntax and Semantics of Abstract Binding Trees. CoRR (2016)
Jonathan Sterling
Primitive Recursive Bars Are Inductive. CoRR (2016)
Jonathan Sterling
Type Theory and its Meaning Explanations. CoRR (2015)
Jonathan Sterling
Remark on the hypothetical judgment. CoRR (2015)
Darryl McAdams, Jonathan Sterling
Dependent Types for Pragmatics. CoRR (2014)