8 citations · 16 across the 8 of their papers we have counts for
11 papers
Nominal Type Theory by Nullary Internal Parametricity
Antoine Van Muylder, Andreas Nuyts, Dominique Devriese
There are many ways to represent the syntax of a language with binders. In particular, nominal frameworks are metalanguages that feature (among others) name abstraction types, whic…
Towards Computational UIP in Cubical Agda
Yee-Jian Tan, Andreas Nuyts, Dominique Devriese
Some advantages of Cubical Type Theory, as implemented by Cubical Agda, over intensional Martin-Löf Type Theory include Quotient Inductive Types (QITs), which exist as instances of…
A Sound and Complete Substitution Algorithm for Multimode Type Theory: Technical Report
Joris Ceulemans, Andreas Nuyts, Dominique Devriese
This is the technical report accompanying the paper "A Sound and Complete Substitution Algorithm for Multimode Type Theory" [Ceulemans, Nuyts and Devriese, 2024]. It contains a ful…
Sikkel: Multimode Simple Type Theory as an Agda Library
Joris Ceulemans, Andreas Nuyts, Dominique Devriese
Many variants of type theory extend a basic theory with additional primitives or properties like univalence, guarded recursion or parametricity, to enable constructions or proofs t…
Parametricity Features and their Requirements
Andreas Nuyts
In this note, we discuss a number of parametricity features and what their requirements are in terms of complexity of the type system and its model.
Multimodal Dependent Type Theory
Daniel Gratzer, G. A. Kavvos, Andreas Nuyts +1
We introduce MTT, a dependent type theory which supports multiple modalities. MTT is parametrized by a mode theory which specifies a collection of modes, modalities, and transforma…
Transpension: The Right Adjoint to the Pi-type
Andreas Nuyts, Dominique Devriese
Presheaf models of dependent type theory have been successfully applied to model HoTT, parametricity, and directed, guarded and nominal type theory. There has been considerable int…
The Transpension Type: Technical Report
Andreas Nuyts
The purpose of these notes is to give a categorical semantics for the transpension type (Nuyts and Devriese, Transpension: The Right Adjoint to the Pi-type, Accepted at LMCS, 2024)…
A categorical approach to secure compilation
Stelios Tsampas, Andreas Nuyts, Dominique Devriese +1
We introduce a novel approach to secure compilation based on maps of distributive laws. We demonstrate through four examples that the coherence criterion for maps of distributive l…
Presheaf Models of Relational Modalities in Dependent Type Theory
Andreas Nuyts
This report is an extension of 'A Model of Parametric Dependent Type Theory in Bridge/Path Cubical Sets' (Nuyts, arXiv:1706.04383). The purpose of this text is to prove all technic…
A Model of Parametric Dependent Type Theory in Bridge/Path Cubical Sets
Andreas Nuyts
The purpose of this text is to prove all technical aspects of our model for dependent type theory with parametric quantifiers [Nuyts, Vezzosi and Devriese, 2017]. It is well-known…