research
∙
12/01/2021
Finitary type theories with and without contexts
We give a definition of finitary type theories that subsumes many exampl...
share
research
∙
03/12/2021
An extensible equality checking algorithm for dependent type theories
We present a general and user-extensible equality checking algorithm tha...
research
∙
09/11/2020
A general definition of dependent type theories
We define a general class of dependent type theories, encompassing Marti...
research
∙
10/25/2019
Runners in action
Runners of algebraic effects, also known as comodels, provide a mathemat...
research
∙
07/16/2018
What is algebraic about algebraic effects and handlers?
This note recapitulates and expands the contents of a tutorial on the ma...
research
∙
04/02/2018
Every metric space is separable in function realizability
We first show that in the function realizability topos every metric spac...
research
∙
02/17/2018