Andreas Nuyts

Andreas Nuyts

Email: firstname dot lastname at kuleuven dot be
Github: anuyts
Mastodon: anuytstt@fosstodon.org
Twitter: anuytstt (synced with Mastodon)

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.

* Please don't print these slides, which have incrementally appearing bullet points.

My research and publications

BibTeX - dblp - Google Scholar - ORCiD

Table of Contents

  1. Posts
  2. Syntax of Type Theory
  3. Multimode and Presheaf Type Theory
  4. Effects in Dependent Type Theory
  5. Categorical Secure Compilation

Posts

Syntax of Type Theory

Contextual Algebraic Theories: Generic Boilerplate beyond Abstraction (Accepted at TyDe '22)

Understanding Universal Algebra Using Kleisli-Eilenberg-Moore-Lawvere Diagrams (2022)

Multimode and Presheaf Type Theory

Transpension: The Right Adjoint to the Pi-type (2021, Submitted to LMCS)
With Dominique Devriese.

Sikkel: Multimode Simple Type Theory as an Agda Library (MSFP 2022)
By Joris Ceulemans, Andreas Nuyts, Dominique Devriese

Extending Cubical Agda with Internal Parametricity (TYPES '22)
By Antoine Van Muylder, Andrea Vezzosi, Andreas Nuyts, Dominique Devriese

A Vision for Natural Type Theory (2020): Note

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

Robust Notions of Contextual Fibrancy (2020)
MTT: Multimodal Dependent Type Theory (LICS '20 / LMCS '21)
By Daniel Gratzer, G. A. Kavvos, Andreas Nuyts, Lars Birkedal Menkar - the multimode presheaf proof assistant
Currently on hold for reasons of performance, although we have not given up on the goal of implementing a multimode presheaf proof assistant.
Degrees of Relatedness (LICS '18)
With Dominique Devriese. Parametric Quantifiers for Dependent Type Theory (ICFP '17)
With Andrea Vezzosi and Dominique Devriese. Towards a Directed Homotopy Type Theory based on 4 Kinds of Variance (Master thesis, 2015)

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

Categorical Secure Compilation

Abstract Congruence Criteria for Weak Bisimilarity (MFCS '21)
By Stelios Tsampas, Christian Williams, Andreas Nuyts, Dominique Devriese, Frank Piessens

A Categorical Approach to Secure Compilation (CMCS '20)
By Stelios Tsampas, Andreas Nuyts, Dominique Devriese, Frank Piessens

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