research
∙
02/17/2023
Type-Theoretic Signatures for Algebraic Theories and Inductive Types
We develop the usage of certain type theories as specification languages...
share
research
∙
09/20/2022
Staged Compilation with Two-Level Type Theory
The aim of staged compilation is to enable metaprogramming in a way such...
research
∙
02/27/2021
Generalized Universe Hierarchies and First-Class Universe Levels
In type theories, universe hierarchies are commonly used to increase the...
research
∙
06/21/2020
Large and Infinitary Quotient Inductive-Inductive Types
Quotient inductive-inductive types (QIITs) are generalized inductive typ...
research
∙
07/17/2019
Shallow Embedding of Type Theory is Morally Correct
There are multiple ways to formalise the metatheory of type theory. For ...
research
∙
02/01/2019