Andreas Nuyts
Andreas Nuyts
Email: firstnamelastname at gmail dot com
I am a postdoctoral researcher at the Software Languages Lab at the Vrije Universiteit Brussel, Belgium, under the supervision of Dominique Devriese. I previously worked at KU Leuven, where I obtained my PhD in August 2020.
Most of my research is about dependent type theory, where I am interested in the theory and implementation of modal and presheaf type theory (particularly directed type theory), as well as side-effects. I am also involved in a line of research, headed by Stelios Tsampas, on categorifying secure compilation.
* Please don't print my slides, which have incrementally appearing bullet points.
My research and publications
(BibTeX
-
dblp
-
ORCID)
Table of Contents
- Multimode and Presheaf Type Theory
- Effects in Dependent Type Theory
- Categorical Secure Compilation
Multimode and Presheaf Type Theory
A Vision for Natural Type Theory (2020): Note
- Part I. Grothendieck Construction Considered Harmful
- Part II. Jets: Higher Equipments or Directed Degrees of Relatedness
Contributions to Multimode and Presheaf Type Theory (PhD thesis, 2020)
Supervisors:
Dominique Devriese,
Frank Piessens,
Committee chair:
Robert Puers,
Other committee members:
Lars Birkedal,
Dan Licata,
Bart Jacobs,
Tom Schrijvers
Robust Notions of Contextual Fibrancy (2020)
Transpension: The Right Adjoint to the Pi-type (2020, Submitted to LMCS)
With Dominique Devriese.
MTT: Multimodal Dependent Type Theory (LICS '20)
By Daniel Gratzer,
G. A. Kavvos,
A. N.,
Lars Birkedal
Menkar - the multimode presheaf proof assistant
Currently on hold for reasons of performance, although we have not given up on the goal of implementing a multimode presheaf proof assistant.
Degrees of Relatedness (LICS '18)
With Dominique Devriese.
Parametric Quantifiers for Dependent Type Theory (ICFP '17)
With Andrea Vezzosi and Dominique Devriese.
Towards a Directed Homotopy Type Theory based on 4 Kinds of Variance (Master thesis, 2015)
-
Thesis
-
Errata
- This thesis investigates higher directed type theory from a syntactic point of view. The approach is very non-formal, departing not from the question "What can we justify semantically?" but "What syntax rules can we intuitively expect?" Consider it an inventory of non-formal ideas.
Effects in Dependent Type Theory
How to do Proofs:
Practically Proving Properties about Effectful Programs' Results (Functional Pearl) (TyDe '19)
By Koen Jacobs, A. N., Dominique Devriese
Categorical Secure Compilation
Abstract Congruence Criteria for Weak Bisimilarity (Submitted to LICS '21)
By Stelios Tsampas, Christian Williams, A. N., Dominique Devriese, Frank Piessens
A Categorical Approach to Secure Compilation (CMCS '20)
By Stelios Tsampas, A. N., Dominique Devriese, Frank Piessens
A Summary on Categorical Contextual Reasoning (ACT '19)
By Stelios Tsampas, A. N., Dominique Devriese, Frank Piessens