Jonathan Sterling

52 papers A* 4B 6Journal 40Unranked 1

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