Antoine Van Muylder

I am a doctor in computer science. I currently live in Brussels. You can email me at antvanmul then at then hotmail then .com. My office at KU Leuven is 200A (cs building), 03.127.

Research positions & studies

I obtained my PhD in KU Leuven (Belgium) under the supervision of Dominique Devriese and Andreas Nuyts. My PhD thesis is about parametricity for dependent type theory.

Before that, I was working as a research engineer at Inria Paris in the Prosecco team, where the F* Verification Language for Effectful Programs is/was being developed. I did my master internship with Catalin Hritcu in the same team (link).

I hold a bachelor's degree in mathematics from Université Libre de Bruxelles, and a master's degree in mathematical logic and theoretical computer science from Université de Paris.

Publications

• Nominal Type Theory by Nullary Internal Parametricity (preprint, accepted at the TYPES25 post-proceedings).
  Van Muylder A., Nuyts A., & Devriese D. (2025).
  ‍
• Internal and Observational Parametricity for Cubical Agda (conference paper).
  Van Muylder A., Nuyts A., & Devriese D. (2024).
  Proceedings of the ACM on Programming Languages, 8(POPL), 209-240. (POPL 2024)
  Accompanying library.
  ‍
• SSProve: A Foundational Framework for Modular Cryptographic Proofs in Coq (journal version).
  Philipp G. Haselwarter, Exequiel Rivas, Antoine Van Muylder, Théo Winterhalter, Carmine Abate, Nikolaj Sidorenco, Catalin Hritcu, Kenji Maillard, Bas Spitters. (2023).
  Transactions on Programming Languages and Systems (TOPLAS).
  ‍
• Extending Cubical Agda with Internal Parametricity (abstract).
  Van Muylder A., Vezzosi A., Nuyts A., & Devriese D. (2022).
  Extended abstract at the TYPES 2022 conference.
  ‍
• SSProve: A Foundational Framework for Modular Cryptographic Proofs in Coq (conference paper).
  Carmine Abate, Philipp G. Haselwarter, Exequiel Rivas, Antoine Van Muylder, Théo Winterhalter, Catalin Hritcu, Kenji Maillard, Bas Spitters. (2021).
  Distinguished paper award at the CSF 2021 symposium.
  Check out our presentations on youtube... (1) (2)
  ‍
• The next 700 relational program logics (conference paper).
  Maillard, K., Hriţcu, C., Rivas, E., & Van Muylder, A. (2019).
  Proceedings of the ACM on Programming Languages, 4(POPL), 1-33.

Interests

I am interested in mathematical unifying theories for logic, computer science, algebra and geometry, as well as in those topics themselves. Here is a non-exhaustive list:

• Type theory, dependent type theory
• Parametricity
• Semantics for type theory
• Proof assistants
• Category theory
• Side effects in programs