28 citations · 116 across the 28 of their papers we have counts for
31 papers
A denotationally-based program logic for higher-order store
Frederik Lerbjerg Aagaard, Jonathan Sterling, Lars Birkedal
Separation logic is used to reason locally about stateful programs. State of the art program logics for higher-order store are usually built on top of untyped operational semantics…
Towards univalent reference types
Jonathan Sterling, Daniel Gratzer, Lars Birkedal
We develop a denotational semantics for general reference types in an impredicative version of guarded homotopy type theory, an adaptation of synthetic guarded domain theory to Voe…
Towards a geometry for syntax
Jonathan Sterling
It often happens that free algebras for a given theory satisfy useful reasoning principles that are not preserved under homomorphisms of algebras, and hence need not hold in an arb…
Decalf: A Directed, Effectful Cost-Aware Logical Framework
Harrison Grodin, Yue Niu, Jonathan Sterling +1
We present Decalf, a directed, effectful cost-aware logical framework for studying quantitative aspects of functional programs with effects. Like Calf, the language is based on an…
On the -topos semantics of homotopy type theory
Emily Riehl
Many introductions to homotopy type theory and the univalence axiom gloss over the semantics of this new formal system in traditional set-based foundations. This expository article…
Reflections on existential types
Jonathan Sterling
Existential types are reconstructed in terms of small reflective subuniverses and dependent sums. The folklore decomposition detailed here gives rise to a particularly simple accou…