Jules Jacobs

Publications

PLDI'25	StacKAT: Infinite State Network Verification Jules Jacobs, Nate Foster, Tobias Kappé, Dexter Kozen, Lily Saada, Alexandra Silva, Jana Wagemaker .pdf demo
OOPSLA'24	Multris: Functional Verification of Multiparty Message Passing in Separation Logic Jonas Kastberg Hinrichsen, Jules Jacobs, Robbert Krebbers .pdf 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 .pdf code
PhD Thesis	Guarantees by Construction Jules Jacobs .pdf code VERSEN 2025 award
POPL'24	Deadlock-Free Separation Logic: Linearity Yields Progress for Dependent Higher-Order Message Passing Jules Jacobs, Jonas Kastberg Hinrichsen, Robbert Krebbers .pdf slides code
ICFP'23	Dependent Session Protocols in Separation Logic from First Principles Jules Jacobs, Jonas Kastberg Hinrichsen, Robbert Krebbers .pdf slides code
POPL'23	Higher-Order Leak and Deadlock Free Locks Jules Jacobs, Stephanie Balzer .pdf slides code bibtex POPL'23 distinguished paper @article{jacobs_locks_2023, author = {Jacobs, Jules and Balzer, Stephanie}, title = {Higher-Order Leak and Deadlock Free Locks}, year = {2023}, volume = {7}, number = {POPL}, doi = {10.1145/3571229}, journal = {Proc. ACM Program. Lang.}, articleno = {36}, }
POPL'23	Fast Coalgebraic Bisimilarity Minimization Jules Jacobs, Thorsten Wißmann .pdf slides code bibtex @article{jacobs_bismin_2023, author = {Jacobs, Jules and Wi\ss{}mann, Thorsten}, title = {Fast Coalgebraic Bisimilarity Minimization}, year = {2023}, volume = {7}, number = {POPL}, doi = {10.1145/3571245}, journal = {Proc. ACM Program. Lang.}, articleno = {52}, }
ICFP'22	Multiparty GV: Functional Multiparty Session Types With Certified Deadlock Freedom Jules Jacobs, Stephanie Balzer, Robbert Krebbers .pdf slides code crossref bibtex @article{jacobs_mpgv_2022, author = {Jacobs, Jules and Balzer, Stephanie and Krebbers, Robbert}, title = {Multiparty GV: Functional Multiparty Session Types with Certified Deadlock Freedom}, year = {2022}, volume = {6}, number = {ICFP}, url = {https://doi.org/10.1145/3547638}, doi = {10.1145/3547638}, journal = {Proc. ACM Program. Lang.}, month = {aug}, }
ECOOP'22	A Self-Dual Distillation of Session Types Jules Jacobs .pdf slides code bibtex @inproceedings{jacobs_distillation_2022, author = {Jacobs, Jules}, title = {{A Self-Dual Distillation of Session Types}}, booktitle = {36th European Conference on Object-Oriented Programming (ECOOP 2022)}, pages = {23:1--23:22}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-225-9}, ISSN = {1868-8969}, year = {2022}, volume = {222}, URL = {https://drops.dagstuhl.de/opus/volltexte/2022/16251}, URN = {urn:nbn:de:0030-drops-162518}, doi = {10.4230/LIPIcs.ECOOP.2022.23}, }
POPL'22	Connectivity Graphs: A Method for Proving Deadlock Freedom Based on Separation Logic Jules Jacobs, Stephanie Balzer, Robbert Krebbers .pdf slides code bibtex @article{jacobs_cgraphs_2022, author = {Jules Jacobs and Stephanie Balzer and Robbert Krebbers}, title = {Connectivity graphs: a method for proving deadlock freedom based on separation logic}, journal = {Proc. {ACM} Program. Lang.}, volume = {6}, number = {{POPL}}, pages = {1--33}, year = {2022}, url = {https://doi.org/10.1145/3498662}, doi = {10.1145/3498662}, }
Neuro-biology 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 bibtex @article{KARA2021, title = {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}, journal = {Neurobiology of Aging}, year = {2021}, issn = {0197-4580}, doi = {https://doi.org/10.1016/j.neurobiolaging.2021.02.011}, url = {https://www.sciencedirect.com/science/article/pii/S019745802100066X}, author = {Firat Kara and Michael E. Belloy and Rick Voncken and Zahra Sarwari and Yadav Garima and Cynthia Anckaerts and An Langbeen and Valerie Leysen and Disha Shah and Jules Jacobs and Julie Hamaide and Peter Bols and Johan {Van Audekerke} and Jasmijn Daans and Caroline Guglielmetti and Kejal Kantarci and Vincent Prevot and Steffen Roßner and Peter Ponsaerts and Annemie {Van der Linden} and Marleen Verhoye}, }
POPL'21	Paradoxes of Probabilistic Programming And How to Condition on Events of Measure Zero with Infinitesimal Probabilities Jules Jacobs .pdf code slides video bibtex @article{jacobs_paradoxes_2021, title = {Paradoxes of probabilistic programming: and how to condition on events of measure zero with infinitesimal probabilities}, volume = {5}, shorttitle = {Paradoxes of probabilistic programming}, doi = {10.1145/3434339}, number = {POPL}, journal = {Proc. {ACM} Program. Lang.}, author = {Jacobs, Jules}, year = {2021}, pages = {58:1--58:26}, }

Collaborators

I'm lucky to work with some great people. Here are some of them:

Alexandra Silva, Cole Schlesinger, David Darais, Dexter Kozen, Ernest Ng, Guy Amir, Jana Wagemaker, Jonas Kastberg Hinrichsen, Katherine Wu, Lily Saada, Mark Barbone, Mark Moeller, Nate Foster, Olivier Savary Belanger, Robbert Krebbers, Steffen Smolka, Stephanie Balzer, Thorsten Wißmann, Tobias Kappé.

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 :)

Oct. 2022	The product of gcd and lcm
Aug. 2022	A multilinear proof of Jacobi's formula
Mar. 2022	A paradoxical local minimum
Feb. 2022	Divisibility of multinomial coefficients
Dec. 2021	Coq cheatsheet
Dec. 2021	The Cartan-Dieudonné theorem
Dec. 2021	Various cute implementations of primitive type and proof checkers in HOAS+LCF style (STLC, bidirectional, System F, FOL, dependent type theory).
Sep. 2021	Bottom-up rewriting with smart constructors, hereditary substitution & normalization by evaluation
Sep. 2021	A quick introduction to quantum programming
Aug. 2021	The sign of a permutation is multiplicative
May 2021	Resampling with infinitesimal probabilities
May 2021	Bounded clause elimination
Apr. 2021	From regex to NFA and back code
Apr. 2021	How to compile pattern matching code
Apr. 2021	Arithmetic on Church numerals using a notational trick code
Apr. 2021	Gentzen's Perspective on Classical versus Intuitionistic Logic: LK vs LJ code
Apr. 2021	Induction on Derivations is Recursion code
Mar. 2021	How to prove normalisation of STLC
Dec. 2020	A simple proof of the matrix-tree theorem, upward routes, and a matrix-tree-cycle theorem
Dec. 2020	Functional Evaluation Contexts An alternative way to handle evaluation contexts in proof assistants like Coq code
Dec. 2020	Sorting Real Numbers, Constructively
Dec. 2020	Binary Search a Little Simpler & More Generic
Sep. 2020	A Magic Determinant Formula for Symmetric Polynomials of Eigenvalues code

You can find some more on my blog.

Talks

6 Feb. 2024	Deadlock-Free Separation Logic: Linearity Yields Progress for Dependent Higher-Order Message Passing EPFL
18 Jan. 2024	Deadlock-Free Separation Logic: Linearity Yields Progress for Dependent Higher-Order Message Passing POPL'24
16 Jan. 2024	Probabilistic Programming Session Preview POPL'24 (session preview)
15 Jan. 2024	Verified Message-Passing Concurrency in Iris: Separation Logic Meets Session Types POPL'24 (tutorial, with Jonas Kastberg Hinrichsen and Robbert Krebbers)
11 Dec. 2023	The Iris Masterplan PL Retreat, Cornell University
20 Sept. 2023	Higher-Order Leak and Deadlock Free Locks Cornell University
14 June 2023	Higher-Order Leak and Deadlock Free Locks Carnegie Mellon University
7 June 2023	Fast Coalgebraic Bisimilarity Minimization Cornell University
22 May. 2023	Dependent Session Protocols in Separation Logic From First Principles Iris Workshop 2023
30 Mar. 2023	Fast Coalgebraic Bisimilarity Minimization LIP ENS Lyon
3 Mar. 2023	Higher-Order Leak and Deadlock Free Locks POPV seminar Boston
17 Feb. 2023	Higher-Order Leak and Deadlock Free Locks LFCS seminar Edinburgh
20 Jan. 2023	Fast Coalgebraic Bisimilarity Minimization POPL'23
18 Jan. 2023	Higher-Order Leak and Deadlock Free Locks POPL'23
25 Oct. 2022	Fast Coalgebraic Bisimilarity Minimization SWS Seminar, Radboud University
22 June 2022	Multiparty GV: Functional Multiparty Session Types With Certified Deadlock Freedom ICFP'22
22 June 2022	A Simple Concurrent Lambda Calculusu For Encoding Session Types TYPES'22
9 June 2022	Paradoxes of Probabilistic Programming PLDI'22 Sigplan Track
9 June 2022	A Self-Dual Distillation of Session Types ECOOP'22
2 May 2022	Connectivity Graphs: A Method for Proving Deadlock Freedom Based on Separation Logic Iris workshop
28 Apr. 2022	Connectivity Graphs: A Method for Proving Deadlock Freedom Based on Separation Logic CMU plunch
25 Mar. 2022	Connectivity Graphs: A Method for Proving Deadlock Freedom Based on Separation Logic Imperial College London
19 Jan. 2022	Connectivity Graphs: A Method for Proving Deadlock Freedom Based on Separation Logic POPL'22
12 Oct. 2021	Mechanized Deadlock Freedom for Session Types FCG, University of Groningen
19 July 2021	Pardoxes of Probabilistic Programming (and deleted scenes) VeriProP'21
12 July 2021	Mechanized Deadlock Fredom for Session Types VEST'21
3 Feb. 2021	Deadlock Freedom for Session Types Using Separation Logic SWS Seminar, Radboud University
22 Jan. 2021	Paradoxes of Probabilistic Programming POPL'21
25 Nov. 2020	Paradoxes of Probabilistic Programming PL Seminar, TU Delft
23 Nov. 2020	Paradoxes of Probabilistic Programming PPLV, University College London
28 Oct. 2020	Paradoxes of Probabilistic Programming SWS Seminar, Radboud University

Teaching

2024	Helping Nate Foster teach Certified Software Systems (CS6115) at Cornell University.
2023	Helping Robbert teach Coq & separation logic in Program Verification course at RU.
2022	Assisting Robbert with the supervision of Menzo van Kessel's bachelor thesis project about implementing a type checker and interpreter for MPGV.
2022	Helping students prepare their presentations for the MFOCS seminar course at RU.
2022	Helping Freek teach Coq in the Type Theory course at RU.
2022	Helping Robbert teach Coq & separation logic in Program Verification course at RU.
2021	Helping Freek teach Coq in the Type Theory course at RU.
2021	Helping students prepare their presentations for the MFOCS seminar course at RU.
2020	Helping Freek teach Coq in the Type Theory course at RU.
2020	Assisting Robbert with the master thesis project of Edoardo Putti about mechanizing incorrectness separation logic in Coq.
2020	Assisting Robbert with the Software Verification course at TU Delft.

Academic Service

2025	ICFP'25 PC
2025	PLDI'25 PC
2025	ECOOP'25 PC
2025	PLACES'25 PC
2025	Website co-chair for ICFP'25
2024	Website co-chair for ICFP'24
2024 - ongoing	PLMW social media chair
2024	Reviewing for ECOOP'24
2023	Reviewing for PLDI'23
2023	Reviewing for ITP'23
2023	Reviewing for LICS'23
2023	ESOP'23 AEC
2022	Reviewing for POPL'23
2022	Reviewing for CSL
2022	Reviewing LMCS
2022	Reviewing OOPSLA
2022	PLDI'22 AEC
2022	ESOP'22 AEC
2021	VCA for Behavioural Types: Bridging Theory and Practice
2020	Reviewing for ESOP'21.
2020	Reviewing for ICFP'20.