Andreas Nuyts

Andreas Nuyts

Email: firstname dot lastname at kuleuven dot be
Github: anuyts
Mastodon: (I review follow requests, see my profile description on Mastodon)

BibTeX - dblp - Google Scholar - ORCiD

Table of Contents

About Me

I am a postdoctoral fellow of the Research Foundation - Flanders (FWO) at imec-DistriNet, KU Leuven, Belgium. I obtained my PhD at this same university in August 2020, and have subsequently worked for 1 year at VUB.

Most of my research is about dependent type theory. There, I am interested in the theory and implementation of modal and presheaf type theory (particularly directed type theory), a quest which also led me to an interest in general syntactic aspects of type theory. I am also fascinated by the question of how to reason about side-effects in dependent type theory. Furthermore, I have been involved in a line of research, headed by Stelios Tsampas, on categorifying secure compilation.

I find it especially motivating to hear from people who are interested in (using) my work, so do not hesitate to contact me in case of questions, remarks or puzzlement about any of my papers, notes or code.

My Research and Publications

* Please don't print these slides, which have incrementally appearing bullet points.

What's New


Syntax of Type Theory

πŸ“‹ Contextual Algebraic Theories: Generic Boilerplate beyond Abstraction (TyDe '22)
πŸ”— Extended Abstract - Slides* - Video - Github

πŸ“œ Understanding Universal Algebra Using Kleisli-Eilenberg-Moore-Lawvere Diagrams (2022)
πŸ”— Note

Multimode and Presheaf Type Theory

General Multimode and Presheaf Type Theory

πŸ“ Transpension: The Right Adjoint to the Pi-type ('20-'23, Submitted to LMCS)
πŸ‘₯ With Dominique Devriese.
πŸ”— Preprint (based on ch. 7 of my PhD thesis) - Technical report

πŸ“‹ A Lock Calculus for Multimode Type Theory (TYPES '23): Abstract - Slides* - Video

πŸ“‹ Every Modality is a Relative Right Adjoint (EPN WG6, 2023): Mini-abstract - Slides*
πŸ‘₯ With Josselin Poiret.

πŸ“„ Sikkel: Multimode Simple Type Theory as an Agda Library (MSFP 2022)
πŸ‘₯ By Joris Ceulemans, Andreas Nuyts, Dominique Devriese
πŸ”— DOI - Github - Slides* - Video

πŸ“• 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)

πŸ“„ MTT: Multimodal Dependent Type Theory (LICS '20 / LMCS '21)
πŸ‘₯ By Daniel Gratzer, G. A. Kavvos, Andreas Nuyts, Lars Birkedal

πŸ’» Menkar - the multimode presheaf proof assistant
Currently on hold for reasons of performance, although I have not given up on the goal of implementing a multimode presheaf proof assistant.

Directed and Naturality Type Theory

πŸ“‹ Read the Mood Mode and Stay Positive (TYPES '23) (Polarity modalities in Agda)
πŸ‘₯ With Josselin Poiret, Lucas Escot, Joris Ceulemans and Malin AltenmΓΌller.
πŸ”— Abstract - Video - Slides* - Pull request

πŸ“‹ Higher Pro-arrows: Towards a Model for Naturality Pretype Theory (HoTT/UF '23)
πŸ”— Abstract - Slides* - Video

πŸ“— Towards a Directed Homotopy Type Theory based on 4 Kinds of Variance (Master thesis, 2015)
πŸ‘₯ Supervisors: Dominique Devriese, Frank Piessens,
πŸ‘€ Mentor: Jesper Cockx,
πŸ”— 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.

Parametricity and Degrees of Relatedness

πŸ“‹ Lax-Idempotent 2-Monads, Degrees of Relatedness, and Multilevel Type Theory (TYPES '23):
πŸ”— Abstract - Slides* - Video
🀦 Erratum: Both abstract and slides mentioned semisimplicial sets where I meant augmented simplicial sets.

πŸ“‹ Extending Cubical Agda with Internal Parametricity (TYPES '22)
πŸ‘₯ By Antoine Van Muylder, Andrea Vezzosi, Andreas Nuyts, Dominique Devriese
πŸ”— Abstract - Slides*

πŸ“„ Degrees of Relatedness (LICS '18)
πŸ‘₯ With Dominique Devriese.
πŸ”— Paper with appendices - Official proceeding - Technical report πŸ“„ Parametric Quantifiers for Dependent Type Theory (ICFP '17)
πŸ‘₯ With Andrea Vezzosi and Dominique Devriese.
πŸ”— Paper - DOI - Slides* - Video - Full artifact

Effects in Dependent Type Theory

πŸ“„ How to do Proofs: Practically Proving Properties about Effectful Programs' Results (Functional Pearl) (TyDe '19)
πŸ‘₯ By Koen Jacobs, Andreas Nuyts, Dominique Devriese
πŸ”— Paper - Code

Categorical Secure Compilation

πŸ“„ Abstract Congruence Criteria for Weak Bisimilarity (MFCS '21): DOI
πŸ‘₯ By Stelios Tsampas, Christian Williams, Andreas Nuyts, Dominique Devriese, Frank Piessens

πŸ“„ A Categorical Approach to Secure Compilation (CMCS '20): DOI - ArXiv
πŸ‘₯ By Stelios Tsampas, Andreas Nuyts, Dominique Devriese, Frank Piessens

πŸ“‹ A Summary on Categorical Contextual Reasoning (ACT '19): Abstract
πŸ‘₯ By Stelios Tsampas, Andreas Nuyts, Dominique Devriese, Frank Piessens


πŸ’» Agda installation

πŸ“— Master theses (mathematics)

πŸ§‘β€πŸ« Presheaf lectures (2022): ToC and references

πŸ§‘β€πŸ« Formal Systems and their Applications