Andreas Nuyts

I obtained my PhD under the supervision of prof. Dominique Devriese and prof. Frank Piessens at imec-DistriNet, KU Leuven, Belgium, holding a PhD fellowship from the Research Foundation - Flanders (FWO).

My research and publications (BibTeX - dblp - ORCID)

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
• 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

• A Categorical Approach to Secure Compilation (CMCS '20)
• Categorical Contextual Reasoning (ACT '19)

• Currently discontinued for reasons of performance. I intend to write up what we can learn from this experience.
• Github
• Abstract - Slides* (TYPES '19)

• Paper

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