Jules Jacobs

blog github twitter mastodon email PL deadlines

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 data flow lattice, generating functions & Kirchoff's matrix-tree theorem, differential forms & the Gauss-Bonnet theorem, star semirings, Lagrangian mechanics.

Publications

POPL'23	Higher-Order Leak and Deadlock Free Locks Jules Jacobs, Stephanie Balzer code
POPL'23	Fast Coalgebraic Bisimilarity Minimization Jules Jacobs, Thorsten Wiẞmann slides code
ICFP'22	Multiparty GV: Functional Multiparty Session Types With Certified Deadlock Freedom Jules Jacobs, Stephanie Balzer, Robbert Krebbers pdf slides code crossref
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}, url = {https://doi.org/10.1145/3434339}, doi = {10.1145/3434339}, number = {POPL}, urldate = {2021-01-11}, journal = {Proceedings of the ACM on Programming Languages}, author = {Jacobs, Jules}, month = jan, year = {2021}, keywords = {probabilistic programming}, pages = {58:1--58:26}, }

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 Jules Jacobs
Aug. 2022	A multilinear proof of Jacobi's formula Jules Jacobs
Mar. 2022	A paradoxical local minimum Jules Jacobs
Feb. 2022	Divisibility of multinomial coefficients Jules Jacobs
Dec. 2021	Coq cheatsheet Jules Jacobs
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 code
Apr. 2021	How to compile pattern matching Jules Jacobs code
Apr. 2021	Arithmetic on Church numerals using a notational trick Jules Jacobs code
Apr. 2021	Gentzen's Perspective on Classical versus Intuitionistic Logic: LK vs LJ Jules Jacobs code
Apr. 2021	Induction on Derivations is Recursion Jules Jacobs code
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 code
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 code

Talks

25 Oct 2022	Fast Coalgebraic Bisimilarity Minimization SWS Seminar
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
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

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.