Jules Jacobs

Research projects

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'26PDFtalkcodeLets OxCaml strengthen the modes of values automatically when their type makes it safe, as for immutable data.
• Stable patterns preprintPDFvideodemoOne analysis that finds what constant propagation, unboxing and closure analysis find separately.
• Vox toolslidescodeChecks specifications at compile time on top of OxCaml, with refinement types and ghost proofs that are erased before code generation.
• OxCaml languageplaygroundcourseJane 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.
• Eggstract toolExtracts shared, acyclic DAGs from e-graphs, with a Rust library, a command-line tool and an optional CP-SAT backend.

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

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'24PDFtalkslidesdemocodeChecks NetKAT network specifications for properties like reachability and isolation, often in under a second.
• StacKAT PLDI'25PDFvideoslidesdemocodeExtends NetKAT with a packet stack, with a decision procedure and complete axioms for program equivalence.
• NEST ECOOP'26PDFcodeEnforces application protocols inside the network, with packet-level monitors generated from session types.
• SER TACAS'26PDFcodeDecides whether programs in the SER language are serializable, giving a certificate or a counterexample.
• Boa POPL'23PDFvideoslidescodeOne generic algorithm that minimizes many kinds of automata up to bisimilarity, also on large systems.
• Petra toolA Petri-net reachability solver.

CollaboratorsNate 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

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

CollaboratorsRobbert Krebbers, Stephanie Balzer and Jonas Kastberg Hinrichsen

Probabilistic programming

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

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

CollaboratorsKatherine Wu, Kevin Batz and Alexandra Silva

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

Teaching

Academic Service

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.

• You Don't Need Matrix Calculus 2024
• Indexing Binary Heaps 2024
• The CAP theorem 2024
• Demystifying lvalues 2024
• Timestamps in UUIDs 2024
• How good are humans at mathematics? 2023
• On battery storage 2023
• Why Coq VMs are useless 2023
• On NaN comparison 2023
• On div and mod 2023
• Deep learning is maximum likelihood 2023
• Generalizing itertools 2023
• The product of gcd and lcm 2022
• A multilinear proof of Jacobi's formula 2022
• A paradoxical local minimum video 2022
• Divisibility of multinomial coefficients 2022
• Coq cheatsheet 2021
• The Cartan-Dieudonné theorem 2021
• Various cute implementations of primitive type and proof checkers in HOAS+LCF style (STLC, bidirectional, System F, FOL, dependent type theory). 2021
• Bottom-up rewriting with smart constructors, hereditary substitution & normalization by evaluation 2021
• A quick introduction to quantum programming 2021
• The sign of a permutation is multiplicative 2021
• Resampling with infinitesimal probabilities 2021
• Bounded clause elimination 2021
• From regex to NFA and back code 2021
• How to compile pattern matching code 2021
• Arithmetic on Church numerals using a notational trick code 2021
• Gentzen's Perspective on Classical versus Intuitionistic Logic: LK vs LJ code 2021
• Induction on Derivations is Recursion code 2021
• How to prove normalisation of STLC 2021
• A simple proof of the matrix-tree theorem, upward routes, and a matrix-tree-cycle theorem 2020
• Functional Evaluation Contexts code 2020
• Sorting Real Numbers, Constructively 2020
• Binary Search a Little Simpler & More Generic 2020
• A Magic Determinant Formula for Symmetric Polynomials of Eigenvalues code 2020
• Stronger unit propagation when solving CSPs with a SAT solver 2019
• Earley parsing in cubic time 2019
• Disambiguation of context free grammars 2019
• Bayes’ rule from minimum relative entropy, and an alternative derivation of variational inference 2019
• Bayes’ rule simply 2019
• Why two’s complement works 2019
• Leapfrog and Verlet are the same method 2019
• Consistent execution of imperative reactive programs 2019
• Proof that the calculus sin and cos functions equal the geometric sin and cos 2019
• Math puzzle: how many coins do you need to toss to maximise the probability of getting 10 heads? 2019
• What is contification? 2019
• Combining probabilities? Try a logarithm. 2018
• Hooks bring React closer to Functional Reactive Programming 2018

Photos

Some of my photos. There are more in the gallery.