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 (OA under Belgian law)  dblp  Google Scholar  ORCiD
Table of Contents
 Table of Contents (you are here)
 About Me
 My Research and Publications
 Teaching
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 compiletime guarantees and proofassistants which can verify humanwritten or computergenerated 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 2level 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 typelevel 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 sideeffects 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
 May 2024: 🧑🏫 I gave a HoTTEST seminar on Naturality Pretype Theory
 Apr 2024: 📝 Transpension: The Right Adjoint to the Pitype accepted at LMCS
 Apr 2024: 🏛️ Hosted & coorganized the EuroProofNet WG6 meeting on Type Theory in Leuven
 Apr 2024: 🏛️ Hosted HoTT/UF 2024 in Leuven
 Feb 2024: 📜 Lifting Profunctors to Presheaf Categories (Note)
 Dec 2023: 📝 Admissibility of Substitution for Multimode Type Theory (Preprint)
 Nov 2023: 📄 Internal and Observational Parametricity for Cubical Agda (POPL 2024)
 Oct 2023: 🔬✍️ First chapter of a technical report on Naturality Pretype Theory
 May 2023: 📋 LaxIdempotent 2Monads, Degrees of Relatedness, and Multilevel Type Theory (TYPES 2023)
 May 2023: 📋 A Lock Calculus for Multimode Type Theory (TYPES 2023)
 May 2023: 📋 Read the
MoodMode and Stay Positive (TYPES 2023)
Category Theory
📜 Lifting Profunctors to Presheaf Categories (Feb '24): Note
📜 Equalityinequalityout 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
 💻 Multisorted Algebraic Theories: Github
📜 Understanding Universal Algebra Using KleisliEilenbergMooreLawvere Diagrams (2022)
🔗 Note
Multimode and Presheaf Type Theory
General Multimode and Presheaf Type Theory
📝 Admissibility of Substitution for Multimode Type Theory (2023)
👥 By Joris Ceulemans, Andreas Nuyts, Dominique Devriese
🔗 Preprint  Technical report
 📋 EPN WG6, 2024: Miniabstract
📝 Transpension: The Right Adjoint to the Pitype ('20'24, accepted at LMCS)
👥 With Dominique Devriese.
🔗 Preprint (based on ch. 7 of my PhD thesis)

Technical report
 📋 Transpension: The Right Adjoint to the Pitype (TYPES '22)
🔗 Abstract (Lirias  Local copy  TYPES copy)  Slides*  📋 Dependable Atomicity in Type Theory (TYPES '19)
🔗 Abstract (Lirias  Local copy)  Slides*  📋 Internalizing Presheaf Semantics: Charting the Design Space (HoTT/UF '18)
🔗 Abstract (Lirias  Local copy)  Slides*
📋 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):
Miniabstract

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
 📋 TYPES '22: Abstract (Lirias  TYPES copy)  Slides*
📄 MTT: Multimodal Dependent Type Theory (LICS '20 / LMCS '21)
👥 By Daniel Gratzer,
G. A. Kavvos,
Andreas Nuyts,
Lars Birkedal
 📄 Journal paper (LICS special issue of LMCS '21)
 📄 LICS paper (Lirias  DOI  Local copy)
 🔬 Technical report (Lirias  Local copy)
📕 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
 Overview (2022)
 Final version:
color pdf

grayscale pdf

Lirias file card
 Ch. 1 "Introduction",
 Sec. 1.2 "Higher Directed Type Theory in Practice",
 Part I "Prerequisites",
 Ch. 2 "Mathematical Prerequisites",
 Sec. 2.3 "Presheaves",
 Sec. 2.4 "Factorization Systems",
 Ch. 3 "Formal Systems and Dependent Type Theory",
 Ch. 4 "Presheaf Models of Dependent Type Theory",
 Ch. 2 "Mathematical Prerequisites",
 Part II "Contributions",
 Ch. 5 "Multimode Type Theory",
 Sec. 5.3 is essentially the ➡️ LICS paper on MTT.
🕰️ The tick notation present in sec. 5.3 but absent in the LICS paper is obsolete and superseded by ➡️ the lock calculus for MTT.
 Sec. 5.3 is essentially the ➡️ LICS paper on MTT.
 Ch. 6 "Presheaf Type Theory",
 Ch. 7 🕰️ "Transpension: the Right Adjoint to the Πtype" is superseded by our ➡️ LMCS submission,
 Ch. 8 "Fibrancy" (Robust notions of contextual fibrancy),
 Ch. 9 "Degrees of Relatedness",
 Sec. 9.5 🕰️ "Parametricity Features and their Requirements" is superseded by ➡️ this note,
 Ch. 5 "Multimode Type Theory",
 Ch. 10 "Conclusion"
 Sec. 10.1.1 "Towards Higher Directed Type Theory",
📜 See also "A Vision for Natural Type Theory".
 Sec. 10.1.1 "Towards Higher Directed Type Theory",
 Ch. 1 "Introduction",
 Public defense: Slides* (for a general nonCS audience)
 Announcement for informed outsiders: English  Nederlands
 📖 See ch. 8 of my PhD thesis (2020).

📋🕰️ HoTT/UF '18 (dated)
🔗 Abstract (Lirias  Local copy  HoTT/UF copy)  Slides* (Local copy  HoTT/UF copy)
Currently on hold for reasons of performance, although I have not given up on the goal of implementing a multimode presheaf proof assistant.
 💻 Github
 📋 Abstract (Lirias  Local copy)  Slides* (TYPES '19)
Directed and Naturality Type Theory
🗂️ Naturality Pretype Theory
 🧑🏫 HoTTEST seminar, May 2024: Slides*  Video
 🔬✍️ Technical report (WIP)  Github
 📋 HoTT/UF '23: Abstract (Lirias  Local copy  HoTT/UF copy)  Slides*  Video
 📜 A Vision for Natural Type Theory (2020): Note
 Part I. Grothendieck Construction Considered Harmful
 Part II. Jets: Higher Equipments or Directed Degrees of Relatedness
📋 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 nonformal, departing not from the question "What can we justify semantically?" but "What syntax rules can we intuitively expect?" Consider it an inventory of nonformal ideas.
 📋 Towards a Directed HoTT with Four Kinds of Variance (HoTT/UF '15): Abstract
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
 📋 Internal and Observational Parametricity for Cubical Agda (HoTT/UF '24)
🔗 Abstract (HoTT/UF copy)  📋 Extending Cubical Agda with Internal Parametricity (TYPES '22)
👥 By Antoine Van Muylder, Andrea Vezzosi, Andreas Nuyts, Dominique Devriese
🔗 Abstract (Lirias  TYPES copy)  Slides*
📋 LaxIdempotent 2Monads, 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.
👥 With Dominique Devriese.
 📄 Extended version: Lirias  Local copy
 📄 LICS proceeding: Lirias  DOI
 🔬 Technical report
 📖 Put in an MTT perspective in (but not superseded by) ch. 9 of my PhD thesis.
 🎞️ Slides CHoCoLa @ ENS Lyon, Jan '19* (1h seminar: parametricity background, details of relation framework, model, structural modality, intersections and unions)
 🎞️ Slides LICS '18* (focus on motivation  cuts straight to details of relation framework)
 🎞️ Slides PLNL '18* (from System F parametricity to current work)
 🎞️ Slides EUTypes meeting Nijmegen*
👥 With Andrea Vezzosi and Dominique Devriese.
🔗 Paper (Lirias  DOI  Local copy)  Slides*  Video  Full artifact
 🔬🕰️ Technical report (Superseded by ➡️ LICS '18 technical report. Version 2 addresses an erratum concerning the reflection rule, and function extensionality for parametric functions)
 💻 Agda 'parametric' branch (by Andrea Vezzosi)
 💻 Agda proofs and example code
 📖 Put in an MTT perspective in (but not superseded by) ch. 9 of my PhD thesis.

📋 Application: Reasoning about Effect Parametricity using Dependent Types (TyDe '19)
👥 By Joris Ceulemans, Andreas Nuyts, Dominique Devriese
🔗 Extended abstract (Lirias  TyDe copy) 📗 Reasoning about Effect Parametricity Using Dependent Types (Master Thesis, 2019):
Thesis

Code
👤 Author: Joris Ceulemans, 👤 Supervisor: Dominique Devriese, 👤 Mentor: Andreas Nuyts.
 📗 Reasoning about Effect Parametricity Using Dependent Types (Master Thesis, 2019):
Thesis

Code
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
 📗 Reasoning about Effects in Dependent Type Theory (Master Thesis, 2018):
Thesis
👤 Author: Koen Jacobs, 👤 Supervisor: Dominique Devriese, 👤 Mentor: Andreas Nuyts.
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)
 💡 Subjects '24'25  '23'24
 🎓 Evaluation criteria
 📖 Reading materials (also relevant background material for anyone interested in our research)
🧑🏫 Presheaf lectures (2022): ToC and references
🧑🏫 Formal Systems and their Applications
 📓 Lecture notes on Dependent Type Theory + CurryHoward sheet: Github
 💻 Learn the Agda basics in three 2hour sessions: Github
* Please don't print these slides, which have incrementally appearing bullet points.