Research projects
Safe and verified systems programming
OxCaml is Jane Street's extension of OCaml for safe, fast systems programming. Its modes track whether a value can escape its stack frame or be shared between threads, and mode crossing lets integers, immutable data and other suitable types skip those restrictions automatically. Vox builds on OxCaml to check specifications at compile time, with refinement types and ghost proofs that are erased before code generation. As AI agents write more of our code, such specifications let people stay in charge of what that code does.
Network verification
KATch checks network configurations for properties such as reachability and isolation, typically in well under a second. StacKAT extends this to unbounded state such as MPLS label stacks, and SER decides whether stateful networked programs are serializable. NEST compiles session-type protocols into monitors that run on programmable switches. These tools rest on fast automata algorithms; Boa, for example, minimizes deterministic, weighted and probabilistic automata with one generic algorithm.
Deadlock freedom and verified concurrency
Programs that communicate over channels or share locks can deadlock. We design type systems and separation logics in which well-typed or verified programs never deadlock, and later work also verifies that programs follow their protocols and compute the right results. All proofs are mechanized in Coq/Rocq using Iris.
Probabilistic programming
When continuous random values only matter through comparisons with constants, Slice rewrites a probabilistic program into a discrete one, so that exact solvers can compute its distribution. In Paradoxes of Probabilistic Programming, I showed how infinitesimal probabilities resolve the paradoxes that arise when a program conditions on an event of probability zero.
Some of this work has found its way into industry:
- Jane Street. I work with Jane Street on OxCaml. Mode crossing is implemented in the OxCaml compiler and deployed in Jane Street's code base, and Vox builds compile-time verification on top of OxCaml.
- Google. Google's open-source NetKAT implementation builds its packet sets and transformers on our verifier KATch.
If your company has software or infrastructure where stronger guarantees would help, I'd be glad to talk about working together, for example on a joint project or by hosting one of my students as an intern. Email me.
Students
Current PhD students. Fabian Lukas Grubmüller.
Prospective PhD students. I'm looking for PhD students who want to work on these topics. Please email me first, with [PhD] in the subject, your CV, a few lines about what you would like to work on and why, and one thing you have made or done that you are proud of: a program, a proof, a project or a piece of writing, with a link if there is one. The formal application goes through the department's doctoral program, or through the Direct Doctorate if you have a bachelor's degree.
Master's theses and semester projects. If you are a student at ETH, I supervise theses and projects in these areas. Email me with [Thesis] in the subject.
A strong mathematical background helps, as does experience with proof assistants, compilers or verification tools.
Publications
BibTeX for all papers: publications.bib
| OOPSLA'26 |
Type-Directed Discretization of Probabilistic Programs
|
| ICFP'26 |
Mode Crossing
|
| ECOOP'26 |
NEST: Network Enforced Session Types
|
| TACAS'26 |
Deciding Serializability in Network Systems
|
| PLDI'25 |
StacKAT: Infinite State Network Verification
|
| OOPSLA'24 |
Multris: Functional Verification of Multiparty Message Passing in Separation Logic
|
| PLDI'24 |
KATch: A Fast Symbolic Verifier for NetKAT
|
| PhD Thesis |
Guarantees by Construction
|
| POPL'24 |
Deadlock-Free Separation Logic: Linearity Yields Progress for Dependent Higher-Order Message Passing
|
| ICFP'23 |
Dependent Session Protocols in Separation Logic from First Principles
|
| POPL'23 |
Higher-Order Leak and Deadlock Free Locks
|
| POPL'23 |
Fast Coalgebraic Bisimilarity Minimization
|
| ICFP'22 |
Multiparty GV: Functional Multiparty Session Types With Certified Deadlock Freedom
|
| ECOOP'22 |
A Self-Dual Distillation of Session Types
|
| POPL'22 |
Connectivity Graphs: A Method for Proving Deadlock Freedom Based on Separation Logic
|
| Neurobiology of Aging |
Long-term ovarian hormone deprivation alters functional connectivity, brain neurochemical profile and white matter integrity in the Tg2576 amyloid mouse model of Alzheimer's disease
Firat Kara,
Michael E. Belloy,
Rick Voncken,
Zahra Sarwari,
Yadav Garima,
Cynthia Anckaerts,
An Langbeen,
Valerie Leysen,
Disha Shah,
Jules Jacobs,
Julie Hamaide,
Peter Bols,
Johan Van Audekerke,
Jasmijn Daans,
Caroline Guglielmetti,
Kejal Kantarci,
Vincent Prevot,
Steffen Roßner,
Peter Ponsaerts,
Annemie Van der Linden,
Marleen Verhoye
DOI
|
| POPL'21 |
Paradoxes of Probabilistic Programming
And How to Condition on Events of Measure Zero with Infinitesimal Probabilities
|
Teaching
| ETH Zürich |
Software Engineering Seminar (2026), with Michalis Kokologiannakis and Ralf Jung. |
| Jane Street |
OxCaml Basics (2026), a three-hour course for interns and engineers. |
| Earlier |
Helped teach Certified Software Systems at Cornell (2024); Program Verification (2022, 2023), Type Theory (2020–2022) and the MFOCS seminar (2021, 2022) at Radboud; and Software Verification at TU Delft (2020). Co-supervised Menzo van Kessel's bachelor thesis on a type checker and interpreter for MPGV (2022) and Edoardo Putti's master thesis on mechanizing incorrectness separation logic in Coq (2020). |
Academic Service
| Organizing |
Iris Workshop 2026 at ISTA, with Michael Sammler |
| Program committees |
POPL'27, CSL'27, TFP'26, ICFP'25, PLDI'25, ECOOP'25, PLACES'25; OOPSLA'26 Review Committee |
| Website chair |
PLDI'27 (co-chair), ICFP'26, ICFP/SPLASH'25 (co-chair), ICFP'25 (co-chair), ICFP'24 (co-chair) |
| PLMW |
Social media chair since 2024; committee of PLMW @ SPLASH/ISSTA'26 |
| Artifact evaluation |
ESOP'23, PLDI'22, ESOP'22 |
| Reviewing |
OOPSLA'27, TOPLAS (2026), ECOOP'24, PLDI'23, ITP'23, LICS'23, POPL'23, OOPSLA (2022), CSL (2022), LMCS (2022), ESOP'21, ICFP'20 |
| Software |
PL deadline calendar, upcoming deadlines for programming languages conferences; Review tool, for writing paper reviews next to the PDF |
| Other |
VCA for Behavioural Types: Bridging Theory and Practice (2021) |
Talks
Notes
I sometimes write up my notes because it makes me think a bit more carefully and helps me remember. If you have any comments, questions, or ideas, don't hesitate to send me an email :) More of my writing is on my blog.
Photos
Some of my photos. There are more in the gallery.
