Antoine Van Muylder

I am a doctor in computer science. You can email me at antvanmul then at then hotmail then .com.

Research positions & studies

I obtained my PhD in KU Leuven (Belgium) under the supervision of Dominique Devriese and Andreas Nuyts. My PhD thesis (link) 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 thesis internship with Catalin Hritcu in the same team (link).

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

Publications

• Nominal Type Theory by Nullary Internal Parametricity (conference paper)
  Antoine Van Muylder, Andreas Nuyts, and Dominique Devriese.
  In 31st International Conference on Types for Proofs and Programs (TYPES 2025).
  Leibniz International Proceedings in Informatics (LIPIcs), Volume 384, pp. 12:1-12:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
  ‍
• 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