Andreas Nuyts

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.

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 (BibTeX - dblp - ORCID)

Table of Contents

1. Multimode and Presheaf Type Theory
2. Effects in Dependent Type Theory
3. 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

• Final version: in color - grayscale
• Public defense: Slides* (for a general non-CS audience)
• Announcement for informed outsiders: English - Nederlands

• See ch. 8 of my PhD thesis.
• Abstract - Slides* (HoTT/UF '18)

• Preprint (based on ch. 7 of my PhD thesis) - Technical report
• Dependable Atomicity in Type Theory (TYPES '19): Abstract - Slides*
• Internalizing Presheaf Semantics: Charting the Design Space (HoTT/UF '18): Abstract - Slides*

• Paper (§5.3 of my PhD thesis) - Technical report
• Journal version (accepted at LICS special issue of LMCS)

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

• Paper with appendices - Official proceeding - Technical report
• Put in a more contemporary (2020) perspective in 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* (dated)

• 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 ch. 9 of my PhD thesis.

• 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

• Paper

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

• DOI - ArXiv

A Summary on Categorical Contextual Reasoning (ACT '19)
By Stelios Tsampas, A. N., Dominique Devriese, Frank Piessens

• Abstract