Antoine Van Muylder

Who am I

Hello! I am a maths and computer science PhD student. I currently live in Brussels. You can email me at antvanmul then at then hotmail then .com. My office at KUL is 200A (cs building), 03.127.

Research positions & studies

I am a PhD student of Dominique Devriese at KU Leuven (KUL). My research is about parametricity for dependent type theories. Described in one sentence, parametricity is the fact that all programs preserve structured relations between their inputs. It is a useful property for program verification.

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. My work there was focused on effectful relational program logics and semantics for those, using relative monads and Dijkstra monads. Relational program logics are tools used to build formal proofs that two effectful programs are related. Such logics are useful to certify cryptographic schemes for instance. 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

• 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