research
∙
07/31/2023
Free theorems from univalent reference types
We develop a denotational semantics for general reference types in an im...
share
research
∙
11/11/2022
Under Lock and Key: A Proof System for a Multimodal Logic
We present a proof system for a multimodal logic, based on our previous ...
research
∙
10/11/2022
Controlling unfolding in type theory
We present a novel mechanism for controlling the unfolding of definition...
research
∙
10/05/2022
Denotational semantics of general store and polymorphism
We contribute the first denotational semantics of polymorphic dependent ...
research
∙
03/24/2022
Unifying cubical and multimodal type theory
In this paper we combine the principled approach to programming with mod...
research
∙
02/24/2022
Strict universes for Grothendieck topoi
Hofmann and Streicher famously showed how to lift Grothendieck universes...
research
∙
02/15/2022
The directed plump ordering
Based on Taylor's hereditarily directed plump ordinals, we define the di...
research
∙
02/11/2022
An inductive-recursive universe generic for small families
We show that it is possible to construct a universe in all Grothendieck ...
research
∙
06/02/2021
Normalization for multimodal type theory
We consider the conversion problem for multimodal type theory (MTT) by 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
∙
11/30/2020
Multimodal Dependent Type Theory
We introduce MTT, a dependent type theory which supports multiple modali...
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