CARVIEW

MOTORHOMES

Select Language

HTTP/2 200 server: GitHub.com content-type: text/html; charset=utf-8 last-modified: Tue, 20 Feb 2024 09:15:35 GMT access-control-allow-origin: * strict-transport-security: max-age=31556952 etag: W/"65d46db7-1944" expires: Sun, 28 Dec 2025 06:58:49 GMT cache-control: max-age=600 content-encoding: gzip x-proxy-cache: MISS x-github-request-id: 88A3:123DE:74CEBD:82EC81:6950D2CC accept-ranges: bytes age: 0 date: Sun, 28 Dec 2025 06:48:49 GMT via: 1.1 varnish x-served-by: cache-bom-vanm7210087-BOM x-cache: MISS x-cache-hits: 0 x-timer: S1766904529.334860,VS0,VE244 vary: Accept-Encoding x-fastly-request-id: 4da1ec2de46cc4082f42a7358e4325347a8b5dc0 content-length: 2564 Antoine Van Muylder

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, Thé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, Thé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

Original Source | Taken Source