research
∙
08/05/2023
A denotationally-based program logic for higher-order store
Separation logic is used to reason locally about stateful programs. Stat...
share
research
∙
07/31/2023
Free theorems from univalent reference types
We develop a denotational semantics for general reference types in an im...
research
∙
07/18/2023
Towards a geometry for syntax
It often happens that free algebras for a given theory satisfy useful re...
research
∙
07/12/2023
Decalf: A Directed, Effectful Cost-Aware Logical Framework
We present decalf, a directed, effectful cost-aware logical framework fo...
research
∙
10/11/2022
Controlling unfolding in type theory
We present a novel mechanism for controlling the unfolding of definition...
research
∙
10/10/2022
Classifying topoi in synthetic guarded domain theory
Several different topoi have played an important role in the development...
research
∙
10/09/2022
What should a generic object be?
Jacobs has proposed definitions for (weak, strong, split) generic object...
research
∙
10/05/2022
Denotational semantics of general store and polymorphism
We contribute the first denotational semantics of polymorphic dependent ...
research
∙
10/03/2022
Reflections on existential types
Existential types are reconstructed in terms of small reflective subuniv...
research
∙
04/20/2022
Sheaf semantics of termination-insensitive noninterference
We propose a new sheaf semantics for secure information flow over a spac...
research
∙
02/24/2022
Strict universes for Grothendieck topoi
Hofmann and Streicher famously showed how to lift Grothendieck universes...
research
∙
02/17/2022
Bilimits in categories of partial maps
The closure of chains of embedding-projection pairs (ep-pairs) under bil...
research
∙
02/15/2022
The directed plump ordering
Based on Taylor's hereditarily directed plump ordinals, we define the di...
research
∙
07/09/2021
A cost-aware logical framework
We present calf, a cost-aware logical framework for studying quantitativ...
research
∙
01/27/2021
Normalization for Cubical Type Theory
We prove normalization for (univalent, Cartesian) cubical type theory, c...
research
∙
12/19/2020
Syntactic categories for dependent type theory: sketching and adequacy
We argue that locally Cartesian closed categories form a suitable doctri...
research
∙
10/16/2020
Logical Relations as Types: Proof-Relevant Parametricity for Program Modules
The theory of program modules is of interest to language designers not o...
research
∙
03/03/2020
A Cubical Language for Bishop Sets
We present XTT, a version of Cartesian cubical type theory specialized f...
research
∙
04/18/2019
Cubical Syntax for Reflection-Free Extensional Equality
We contribute XTT, a cubical reconstruction of Observational Type Theory...
research
∙
02/23/2019
Algebraic Type Theory and Universe Hierarchies
It is commonly believed that algebraic notions of type theory support on...
research
∙
09/23/2018
Normalization by gluing for free λ-theories
The connection between normalization by evaluation, logical predicates a...
research
∙
07/05/2018
The RedPRL Proof Assistant (Invited Paper)
RedPRL is an experimental proof assistant based on Cartesian cubical com...
research
∙
04/24/2018