Hi, I am Jules Jacobs. I am in the final year of my PhD program at Radboud University, working on formal verification and programming languages under Robbert Krebbers. Additionally, I am investigating deadlock freedom with Stephanie Balzer.

Some of my favourite things are: type theory, parametricity, SSA as a dataflow lattice, generating functions & Kirchoff's matrix-tree theorem, differential forms & the Gauss-Bonnet theorem, star semirings, Lagrangian mechanics.
Jules

Publications

POPL'23 Higher-Order Leak and Deadlock Free Locks
Jules Jacobs, Stephanie Balzer
.pdf slides code bibtex distinguished paper
POPL'23 Fast Coalgebraic Bisimilarity Minimization
Jules Jacobs, Thorsten Wißmann
.pdf slides code bibtex
ICFP'22 Multiparty GV: Functional Multiparty Session Types With Certified Deadlock Freedom
Jules Jacobs, Stephanie Balzer, Robbert Krebbers
.pdf slides code crossref bibtex
ECOOP'22 A Self-Dual Distillation of Session Types
Jules Jacobs
.pdf slides code bibtex
POPL'22 Connectivity Graphs: A Method for Proving Deadlock Freedom Based on Separation Logic
Jules Jacobs, Stephanie Balzer, Robbert Krebbers
.pdf slides code bibtex
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
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

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 old blog.

Talks

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

2022 Assisting Robbert with the bachelor thesis project of Menzo van Kessel 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

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.