Andreas Nuyts

Andreas Nuyts

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

Pronunciation: /ɑnd'reɑs/ /'nœyts/ or /'nœːts/ (but Noits /'nɔits/ is good enough)
Grammatical gender: masculine (but I'm ok with neutral wordings, esp. when my name stands for a citation)

BibTeX - Lirias (some OA under Belgian law) - dblp - Google Scholar - ORCiD

Table of Contents

About Me

I am a postdoctoral fellow of the Research Foundation - Flanders (FWO) at 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. This domain, which is on the border between mathematical logic and theoretical computer science, is concerned with the development, implementation, semantics and metatheory of dependently typed languages, which are at the same time programming languages with strong compile-time guarantees and proof-assistants which can verify human-written or computer-generated proofs algorithmically.

There, I am interested in the theory and implementation of modal and presheaf type theory (particularly directed type theory). Modal type theory extends type systems essentially with underspecified unary type formers, which can be relevant in a wide range of applications. By presheaf type theory, I refer to the study of presheaf models of type theory and the extension of type systems with language primitives that can be justified specifically by such models. Presheaf models are used to model homotopy type theory (HoTT), parametricity, directed type theory, guarded type theory and 2-level type theory. They also help out in metatheoretical arguments (e.g. to prove normalization) and can be used to simplify working with logical relations via Synthetic Tait Computability. Directed type theory is concerned with providing language support for functoriality of type-level operations. If this language support interacts well with similar support from HoTT (functoriality w.r.t. isomorphisms) and parametricity (w.r.t. relations), then I call this naturality type theory.

The above interest 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

What's New

Category Theory

📜 Lifting Profunctors to Presheaf Categories (Feb '24): Note

📜 Equality-in-equality-out category theory in cubical Agda (Jul '22): Note

Syntax of Type Theory

📋 Contextual Algebraic Theories: Generic Boilerplate beyond Abstraction (TyDe '22)
🔗 Extended Abstract (Lirias - Local Copy) - 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

📄 A Sound and Complete Substitution Algorithm for Multimode Type Theory (TYPES '23 post-proceedings, 2024)
👥 By Joris Ceulemans, Andreas Nuyts, Dominique Devriese
🔗 Paper (DOI - Lirias) - Technical report

📄 Transpension: The Right Adjoint to the Pi-type (LMCS '24 - submitted in '20)
👥 With Dominique Devriese.
🔗 Paper (LMCS/DOI - Lirias - ArXiv - Local copy) - based on ch. 7 of my PhD thesis
🔬 Technical report (ArXiv - Local copy)

📋 A Lock Calculus for Multimode Type Theory (TYPES '23)
🔗 Abstract (Lirias - Local copy) - Slides* - Video

📋 Every Modality is a Relative Right Adjoint (EPN WG6, 2023): Mini-abstract - Slides*
👥 With Josselin Poiret.

📜 Proposal: Multimode Agda (AIM Nov '22): Note

📄 Sikkel: Multimode Simple Type Theory as an Agda Library (MSFP 2022)
👥 By Joris Ceulemans, Andreas Nuyts, Dominique Devriese
🔗 DOI - Github - Slides* - Video

📄 MTT: Multimodal Dependent Type Theory (LICS '20 / LMCS '21)
👥 By Daniel Gratzer, G. A. Kavvos, Andreas Nuyts, Lars Birkedal

📕 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)
💻 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

🗂️ Naturality Pretype 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

📗 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

📄 Internal and Observational Parametricity for Cubical Agda (POPL '24)
👥 By Antoine Van Muylder, Andreas Nuyts, Dominique Devriese
🔗 Paper (Lirias - Local copy - DOI) - Agda branch - Internal library

📋 Lax-Idempotent 2-Monads, Degrees of Relatedness, and Multilevel Type Theory (TYPES '23):
🔗 Abstract (Lirias - Local copy) - Slides* - Video
🤦 Erratum: Both abstract and slides mentioned semisimplicial sets where I meant augmented simplicial sets.

📄 Degrees of Relatedness (LICS '18)
👥 With Dominique Devriese. 📄 Parametric Quantifiers for Dependent Type Theory (ICFP '17)
👥 With Andrea Vezzosi and Dominique Devriese.
🔗 Paper (Lirias - DOI - Local copy) - Slides* - Video - Full artifact

Effects in Dependent Type Theory

🦪 How to do Proofs: Practically Proving Properties about Effectful Programs' Results (TyDe '19)
👥 By Koen Jacobs, Andreas Nuyts, Dominique Devriese
🔗 Functional pearl (Lirias - DOI - Local copy) - Code

Categorical Secure Compilation

📄 Abstract Congruence Criteria for Weak Bisimilarity (MFCS '21): Lirias - DOI
👥 By Stelios Tsampas, Christian Williams, Andreas Nuyts, Dominique Devriese, Frank Piessens

📄 A Categorical Approach to Secure Compilation (CMCS '20): Lirias - DOI - ArXiv
👥 By Stelios Tsampas, Andreas Nuyts, Dominique Devriese, Frank Piessens

📋 A Summary on Categorical Contextual Reasoning (ACT '19): Abstract (Lirias - ACT copy)
👥 By Stelios Tsampas, Andreas Nuyts, Dominique Devriese, Frank Piessens

Teaching

📗 Master theses (mathematics)

🧑‍🏫 Formal Systems and their Applications

🧑‍🏫 Presheaf lectures (2022): ToC and references

ℹ️ Practicalities

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