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)

BibTeX - dblp - Google Scholar - ORCiD

Table of Contents

• Table of Contents (you are here)
• About Me
• My Research and Publications
  1. What's New
  2. Posts
  3. Syntax of Type Theory
  4. Multimode and Presheaf Type Theory
     1. General Multimode and Presheaf Type Theory
     2. Directed and Naturality Type Theory
     3. Parametricity and Degrees of Relatedness
  5. Effects in Dependent Type Theory
  6. Categorical Secure Compilation
• Teaching

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

• Oct 2023: 🌱 First chapter of a technical report on Naturality Pretype Theory
• May 2023: 📝 New version of transpension paper and technical report
• May 2023: 📋 Lax-Idempotent 2-Monads, Degrees of Relatedness, and Multilevel Type Theory (TYPES 2023)
• May 2023: 📋 A Lock Calculus for Multimode Type Theory (TYPES 2023)
• May 2023: 📋 Read the Mood Mode and Stay Positive (TYPES 2023)
• Apr 2023: 📋 Every Modality is a Relative Right Adjoint (EPN WG6, 2023)
• Apr 2023: 📋 Higher Pro-arrows: Towards a Model for Naturality Pretype Theory (HoTT/UF 2023)

Posts

• Equality-in-equality-out category theory in cubical Agda (Jul '22)

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

• 📋 Transpension: The Right Adjoint to the Pi-type (TYPES '22): Abstract - Slides*
• 📋 Dependable Atomicity in Type Theory (TYPES '19): Abstract - Slides*
• 📋 Internalizing Presheaf Semantics: Charting the Design Space (HoTT/UF '18): Abstract - Slides*

📋 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

• 📋 TYPES '22: Abstract - Slides*

📕 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",
  • 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.
  • 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. 10 "Conclusion"
    • Sec. 10.1.1 "Towards Higher Directed Type Theory",
      📜 See also "A Vision for Natural Type Theory".
• Public defense: Slides* (for a general non-CS audience)
• Announcement for informed outsiders: English - Nederlands

📁 Robust Notions of Contextual Fibrancy (2020)

• 📖 See ch. 8 of my PhD thesis (2020).
• 📋🕰️ HoTT/UF '18: Abstract - Slides* (dated)

📄 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 (§5.3 of my PhD thesis) - Technical report

💻 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.

• 💻 Github
• 📋 Abstract - Slides* (TYPES '19)

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

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

📋 Higher Pro-arrows: Towards a Model for Naturality Pretype Theory (HoTT/UF '23)
🔗 Abstract - Slides* - Video

• 🌱 Naturality Pretype Theory: Technical report (WIP) - Github
• 📜 A Vision for Natural Type Theory (2020): Note
  • Part I. Grothendieck Construction Considered Harmful
  • Part II. Jets: Higher Equipments or Directed Degrees of Relatedness

📗 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

• 📖 Put in a more contemporary (2020) 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*

📄 Parametric Quantifiers for Dependent Type Theory (ICFP '17)
👥 With Andrea Vezzosi and Dominique Devriese.
🔗 Paper - DOI - 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 a more contemporary (2020) perspective in (but not superseded by) ch. 9 of my PhD thesis.

• 📋 Application: Reasoning about Effect Parametricity using Dependent Types (TyDe '19): Extended abstract
  👥 By Joris Ceulemans, Andreas Nuyts, Dominique Devriese

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

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

• 📗 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): 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

Teaching

💻 Agda installation

📗 Master theses (mathematics)

• 💡 Subjects '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 + Curry-Howard sheet: Github
• 💻 Learn the Agda basics in three 2-hour sessions: Github