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.

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 (submitted)

• 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