Jules Jacobs


blog github twitter

I'm a PhD student of Robbert Krebbers at Radboud University studying formal verification and programming languages, and working on deadlock freedom in collaboration 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.


POPL'22 Connectivity Graphs: A Method for Proving Deadlock Freedom Based on Separation Logic
Jules Jacobs, Stephanie Balzer, Robbert Krebbers
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
POPL'21 Paradoxes of Probabilistic Programming
And How to Condition on Events of Measure Zero with Infinitesimal Probabilities
Jules Jacobs
pdf acm dl bibtex code slides video


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

Dec. 2021 The Cartan-Dieudonné theorem
Jules Jacobs
Sep. 2021 Bottom-up rewriting with smart constructors, hereditary substitution & normalization by evaluation
Jules Jacobs
Sep. 2021 A quick introduction to quantum programming
Jules Jacobs
Aug. 2021 The sign of a permutation is multiplicative
Jules Jacobs
May. 2021 Resampling with infinitesimal probabilities
Jules Jacobs
May. 2021 Bounded clause elimination
Jules Jacobs
Apr. 2021 From regex to NFA and back
Jules Jacobs
Apr. 2021 How to compile pattern matching
Jules Jacobs
Apr. 2021 Arithmetic on Church numerals using a notational trick
Jules Jacobs
Apr. 2021 Gentzen's Perspective on Classical versus Intuitionistic Logic: LK vs LJ
Jules Jacobs
Apr. 2021 Induction on Derivations is Recursion
Jules Jacobs
Mar. 2021 How to prove normalisation of STLC
Jules Jacobs
Dec. 2020 A simple proof of the matrix-tree theorem, upward routes, and a matrix-tree-cycle theorem
Jules Jacobs
Dec. 2020 Functional Evaluation Contexts
An alternative way to handle evaluation contexts in proof assistants like Coq
Jules Jacobs
Dec. 2020 Sorting Real Numbers, Constructively
Jules Jacobs
Dec. 2020 Binary Search a Little Simpler & More Generic
Jules Jacobs
Sep. 2020 A Magic Determinant Formula for Symmetric Polynomials of Eigenvalues
Jules Jacobs


12 Oct 2021 Mechanized Deadlock Freedom for Session Types
FCG, University of Groningen
19 July 2021 Pardoxes of Probabilistic Programming (and deleted scenes)
12 July 2021 Mechanized Deadlock Fredom for Session Types
3 Feb 2021 Deadlock Freedom for Session Types Using Separation Logic
SWS Seminar
22 Jan 2021 Paradoxes of Probabilistic Programming
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


2021 Assisting with the Type Theory course at RU.
2021 Assisting with the MFOCS seminar at RU.
2020 Assisting with the Type Theory course at RU.
2020 Assisting Robbert Krebbers with the supervision of a master thesis project.
2020 Assisted Robbert Krebbers with the Software Verification course at TU Delft.

Academic Service

2021VCA for Behavioural Types: Bridging Theory and Practice
2020Reviewer for ESOP'21.
2020Reviewer for ICFP'20.