Research projects
Safe and verified systems programming
The goal is systems code that is fast, safe, and checked against its specification. For safety, the modes of OxCaml, Jane Street's extension of OCaml, 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. For verification, Vox, built on OxCaml, checks specifications at compile time, with refinement types and ghost proofs that are erased before code generation. For speed, stable patterns give a compiler one analysis in place of constant propagation, unboxing and closure analysis, so that code written with folds, streams and closures compiles to plain loops. As AI agents write more of our code, checked specifications let people stay in charge of what that code does.
Network verification and automata
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.
Other software. Eggstract extracts shared, acyclic DAGs from e-graphs, with a Rust library, a command-line tool and an optional CP-SAT backend.
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. Want to build proof assistants, verifiers, type systems or programming languages as a PhD student? 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
| Preprint |
Dataflow Facts as Stable Patterns
One analysis that finds what constant propagation, unboxing and closure analysis find separately.
|
| OOPSLA'26 |
Type-Directed Discretization of Probabilistic Programs
Rewrites continuous probabilistic programs into equivalent discrete ones that exact inference engines can run.
|
| ICFP'26 |
Mode Crossing
Lets OxCaml strengthen the modes of values automatically when their type makes it safe, as for immutable data.
|
| ECOOP'26 |
NEST: Network Enforced Session Types
Enforces application protocols inside the network, with packet-level monitors generated from session types.
|
| TACAS'26 |
Deciding Serializability in Network Systems
Decides whether programs in the SER language are serializable, giving a certificate or a counterexample.
|
| PLDI'25 |
StacKAT: Infinite State Network Verification
Extends NetKAT with a packet stack, with a decision procedure and complete axioms for program equivalence.
|
| OOPSLA'24 |
Multris: Functional Verification of Multiparty Message Passing in Separation Logic
A separation logic for proving programs correct that mix multiparty message passing with shared memory.
|
| PLDI'24 |
KATch: A Fast Symbolic Verifier for NetKAT
Checks NetKAT network specifications for properties like reachability and isolation, often in under a second.
|
| PhD Thesis |
Guarantees by Construction
Languages and logics in which deadlock freedom, leak freedom and other guarantees follow by construction.
|
| POPL'24 |
Deadlock-Free Separation Logic: Linearity Yields Progress for Dependent Higher-Order Message Passing
A separation logic for message passing in which deadlock and leak freedom follow from linearity alone.
|
| ICFP'23 |
Dependent Session Protocols in Separation Logic from First Principles
Builds dependent session protocols in separation logic on one-shot channels, in under 1000 lines of Coq.
|
| POPL'23 |
Higher-Order Leak and Deadlock Free Locks
A λ-calculus with higher-order locks in which well-typed programs cannot deadlock or leak memory.
|
| POPL'23 |
Fast Coalgebraic Bisimilarity Minimization
One generic algorithm that minimizes many kinds of automata up to bisimilarity, also on large systems.
|
| ICFP'22 |
Multiparty GV: Functional Multiparty Session Types With Certified Deadlock Freedom
A functional language with multiparty session types in which well-typed programs are deadlock free.
|
| ECOOP'22 |
A Self-Dual Distillation of Session Types
Adds only a fork construct to linear λ-calculus: enough to encode session types, and deadlock free.
|
| POPL'22 |
Connectivity Graphs: A Method for Proving Deadlock Freedom Based on Separation Logic
A method, mechanized in Coq, for proving that concurrent languages are free of deadlocks and memory leaks.
|
| 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
Removes paradoxes of conditioning on measure-zero events by tracking 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 :) Posts from before 2018 are on my blog.
Photos
Some of my photos. There are more in the gallery.
