28 citations · 116 across the 28 of their papers we have counts for
4 papers · 1 filter
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…