Jules Jacobs

Research projects

What Vox adds to OxCaml's modes: a totality axis (partial, total) for specs and lemmas, a ghostliness axis (ghost, real) for erased proofs, and the void layout for free ghost data. Below it, three stable patterns: loop(?i, 1), loop(?i, (?s, u)) and app(inc⟨u⟩), one analysis for fast code.

Safe and verified systems programming

The goal is systems code that is fast, safe, and checked against its specification. As AI agents write more of our code, checked specifications let people stay in charge of what that code does.

Mode Crossing ICFP'26Lets OxCaml strengthen the modes of values automatically when their type makes it safe, as for immutable data.
Stable patterns preprintvideo demoOne analysis that finds what constant propagation, unboxing and closure analysis find separately.
Vox tooltalk codeChecks specifications at compile time on top of OxCaml, with refinement types and ghost proofs that are erased before code generation.
OxCaml languageplayground courseJane 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.

WithBenjamin Peters, Diana Kalinichenko, Liam Stevenson, Aspen Smith, Derek Dreyer, Richard A. Eisenberg and Fabian Lukas Grubmüller

A symbolic packet program from the KATch paper (Fig. 3): a decision diagram over the header fields a, b and c, with dashed edges for the default case.

Network verification and automata

We build verifiers that answer questions about networks, such as reachability and isolation, typically in well under a second, and the automata algorithms that they rest on.

KATch PLDI'24playground slides codeChecks NetKAT network specifications for properties like reachability and isolation, often in under a second.
StacKAT PLDI'25demo slidesExtends NetKAT with a packet stack, with a decision procedure and complete axioms for program equivalence.
NEST ECOOP'26codeEnforces application protocols inside the network, with packet-level monitors generated from session types.
SER TACAS'26codeDecides whether programs in the SER language are serializable, giving a certificate or a counterexample.
Boa POPL'23slides codeOne generic algorithm that minimizes many kinds of automata up to bisimilarity, also on large systems.
Petra toolA Petri-net reachability solver.

WithNate Foster, Alexandra Silva, Jana Wagemaker, Guy Amir, Mark Moeller, Tobias Kappé, Dexter Kozen, Lily Saada, Ernest Ng, Jens Kanstrup Larsen, Alceste Scalas, Mark Barbone, Nicolas Amat, Olivier Savary Belanger, David Darais, Cole Schlesinger, Steffen Smolka and Thorsten Wißmann

A connectivity graph from the paper (Fig. 1): threads T, T1 and T2 and channels C1 and C2, with red triangles showing which endpoint each blocked party is waiting on.

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.

Connectivity graphs POPL'22slides codeA method, mechanized in Coq, for proving that concurrent languages are free of deadlocks and memory leaks.
Multiparty GV ICFP'22slides codeA functional language with multiparty session types in which well-typed programs are deadlock free.
Self-dual session types ECOOP'22slides codeAdds only a fork construct to linear λ-calculus: enough to encode session types, and deadlock free.
Locks POPL'23slides codeA λ-calculus with higher-order locks in which well-typed programs cannot deadlock or leak memory.
Session protocols ICFP'23slides codeBuilds dependent session protocols in separation logic on one-shot channels, in under 1000 lines of Coq.
Deadlock-free separation logic POPL'24slides codeA separation logic for message passing in which deadlock and leak freedom follow from linearity alone.
Multris OOPSLA'24slides codeA separation logic for proving programs correct that mix multiparty message passing with shared memory.
PhD thesis 2024codeLanguages and logics in which deadlock freedom, leak freedom and other guarantees follow by construction.

WithRobbert Krebbers, Stephanie Balzer and Jonas Kastberg Hinrichsen

Discretization from the Slice paper (Fig. 2): a Gaussian sample compared against 0.1, 0.8 and 2.0 becomes a discrete distribution over four intervals.

Probabilistic programming

What a probabilistic program means, and how to compute its distribution exactly.

Slice OOPSLA'26slidesRewrites continuous probabilistic programs into equivalent discrete ones that exact inference engines can run.
Paradoxes POPL'21slides video codeRemoves paradoxes of conditioning on measure-zero events by tracking infinitesimal probabilities.

WithKatherine Wu, Kevin Batz and Alexandra Silva

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 Fabian Lukas Grubmüller, Jules Jacobs One analysis that finds what constant propagation, unboxing and closure analysis find separately. .pdf video demo
OOPSLA'26	Type-Directed Discretization of Probabilistic Programs Katherine Wu, Jules Jacobs, Kevin Batz, Alexandra Silva Rewrites continuous probabilistic programs into equivalent discrete ones that exact inference engines can run. .pdf DOI slides
ICFP'26	Mode Crossing Benjamin Peters, Jules Jacobs, Diana Kalinichenko, Liam Stevenson, Aspen Smith, Derek Dreyer, Richard A. Eisenberg Lets OxCaml strengthen the modes of values automatically when their type makes it safe, as for immutable data. .pdf DOI
ECOOP'26	NEST: Network Enforced Session Types Jens Kanstrup Larsen, Alceste Scalas, Guy Amir, Jules Jacobs, Jana Wagemaker, Nate Foster Enforces application protocols inside the network, with packet-level monitors generated from session types. .pdf DOI arXiv code
TACAS'26	Deciding Serializability in Network Systems Guy Amir, Mark Barbone, Nicolas Amat, Jules Jacobs Decides whether programs in the SER language are serializable, giving a certificate or a counterexample. .pdf DOI arXiv
PLDI'25	StacKAT: Infinite State Network Verification Jules Jacobs, Nate Foster, Tobias Kappé, Dexter Kozen, Lily Saada, Alexandra Silva, Jana Wagemaker Extends NetKAT with a packet stack, with a decision procedure and complete axioms for program equivalence. .pdf DOI slides demo
OOPSLA'24	Multris: Functional Verification of Multiparty Message Passing in Separation Logic Jonas Kastberg Hinrichsen, Jules Jacobs, Robbert Krebbers A separation logic for proving programs correct that mix multiparty message passing with shared memory. .pdf DOI code
PLDI'24	KATch: A Fast Symbolic Verifier for NetKAT Mark Moeller, Jules Jacobs, Olivier Savary Belanger, David Darais, Cole Schlesinger, Steffen Smolka, Nate Foster, Alexandra Silva (* equal contribution) Checks NetKAT network specifications for properties like reachability and isolation, often in under a second. .pdf DOI code
PhD Thesis	Guarantees by Construction Jules Jacobs Languages and logics in which deadlock freedom, leak freedom and other guarantees follow by construction. .pdf DOI code VERSEN 2025 award IPA Dissertation Award 2024
POPL'24	Deadlock-Free Separation Logic: Linearity Yields Progress for Dependent Higher-Order Message Passing Jules Jacobs, Jonas Kastberg Hinrichsen, Robbert Krebbers A separation logic for message passing in which deadlock and leak freedom follow from linearity alone. .pdf DOI slides code
ICFP'23	Dependent Session Protocols in Separation Logic from First Principles Jules Jacobs, Jonas Kastberg Hinrichsen, Robbert Krebbers Builds dependent session protocols in separation logic on one-shot channels, in under 1000 lines of Coq. .pdf DOI slides code
POPL'23	Higher-Order Leak and Deadlock Free Locks Jules Jacobs, Stephanie Balzer A λ-calculus with higher-order locks in which well-typed programs cannot deadlock or leak memory. .pdf DOI slides code POPL'23 distinguished paper
POPL'23	Fast Coalgebraic Bisimilarity Minimization Jules Jacobs, Thorsten Wißmann One generic algorithm that minimizes many kinds of automata up to bisimilarity, also on large systems. .pdf DOI slides code
ICFP'22	Multiparty GV: Functional Multiparty Session Types With Certified Deadlock Freedom Jules Jacobs, Stephanie Balzer, Robbert Krebbers A functional language with multiparty session types in which well-typed programs are deadlock free. .pdf DOI slides code crossref
ECOOP'22	A Self-Dual Distillation of Session Types Jules Jacobs Adds only a fork construct to linear λ-calculus: enough to encode session types, and deadlock free. .pdf DOI slides code
POPL'22	Connectivity Graphs: A Method for Proving Deadlock Freedom Based on Separation Logic Jules Jacobs, Stephanie Balzer, Robbert Krebbers A method, mechanized in Coq, for proving that concurrent languages are free of deadlocks and memory leaks. .pdf DOI slides code
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 Jules Jacobs Removes paradoxes of conditioning on measure-zero events by tracking infinitesimal probabilities. .pdf DOI code slides video

Teaching

ETH Zürich	Research Topics in Software Engineering (2026), with Michalis Kokologiannakis and Ralf Jung.
Jane Street	OxCaml Basics (2026), a three-hour course for interns and engineers.
Cornell	Co-taught Certified Software Systems (2024) with Nate Foster.
Earlier	Helped teach Program Verification (2022, 2023), Type Theory (2020–2022) and the MFOCS seminar (2021, 2022) at Radboud; and Software Verification at TU Delft (2020). Helped develop materials for a verification and separation logic course at Radboud. 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, HOPE'24; PLDI'27 and OOPSLA'26 Review Committees
Website chair	ICFP'27 (co-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; created the PLMW website (2025); committee of PLMW @ SPLASH/ISSTA'26
Mentoring	SIGPLAN-M mentor (2023–2026)
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

2026	Guarantees by construction, revisited IPA Fall Days 2026 · Dissertation Award talk
2026	Vox: Verified OxCaml September 2026
2025	StacKAT: Infinite State Network Verification PLDI'25
2025	Reasoning about Equivalence HKUST · 31 March 2025
2025	Deadlock and Resource Leak Free Languages University of Washington · 27 February 2025
2024	Deadlock-Free Separation Logic: Linearity Yields Progress for Dependent Higher-Order Message Passing EPFL · POPL'24
2024	Probabilistic Programming Session Preview POPL'24 (session preview)
2024	Verified Message-Passing Concurrency in Iris: Separation Logic Meets Session Types POPL'24 (tutorial, with Jonas Kastberg Hinrichsen and Robbert Krebbers)
2023	The Iris Masterplan PL Retreat, Cornell University
2023	Higher-Order Leak and Deadlock Free Locks Cornell University · Carnegie Mellon University · POPV seminar Boston · LFCS seminar Edinburgh · POPL'23
2022–23	Fast Coalgebraic Bisimilarity Minimization Cornell University · LIP ENS Lyon · POPL'23 · SWS Seminar, Radboud University
2023	Dependent Session Protocols in Separation Logic from First Principles Iris Workshop 2023
2022	Multiparty GV: Functional Multiparty Session Types With Certified Deadlock Freedom ICFP'22
2022	A Simple Concurrent Lambda Calculus for Encoding Session Types TYPES'22
2020–22	Paradoxes of Probabilistic Programming PLDI'22 SIGPLAN Track · VeriProP'21 · POPL'21 · PL Seminar, TU Delft · PPLV, University College London · SWS Seminar, Radboud University
2022	A Self-Dual Distillation of Session Types ECOOP'22
2022	Connectivity Graphs: A Method for Proving Deadlock Freedom Based on Separation Logic Iris Workshop · CMU plunch · Imperial College London · POPL'22
2021	Mechanized Deadlock Freedom for Session Types FCG, University of Groningen · VEST'21
2021	Deadlock Freedom for Session Types Using Separation Logic SWS Seminar, Radboud University

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.

A clear turquoise mountain lake with a large boulder

Wild horses at a pond in a nature reserve

A mountain ridge with reddish grass under a blue sky

Frosted trees along a path on a cold morning

A branch with red berries in front of a lake