I am currently doing a PhD in computer science at École Polytechnique, supervised by Samuel Mimram and Éric Goubault.

I study geometric semantics of concurrent programs, and links to the computability of concurrent tasks.

Previously, I was a student at ÉNS Lyon.

- Concurrency
- Geometry, (algebraic) topology
- Category theory
- Semantics of programming languages
- Logic, λ-calculus, type theory
- Formal languages and automata

- 2016: internship at Ludwig-Maximilians University (LMU), Munich, supervised by Martin Hofmann.
*Higher-order model checking of Büchi properties.*[LICS'17 paper] [some slides]*A quantitative model for λ-calculus.*[some notes]

- M2 (2015):
*Sub-extensional type theory*at Université Paris 7, supervised by Hugo Herbelin. [report] [slides (fr)] - M1 (2014):
*Modeling set theory in homotopy type theory*at Radboud University, Nijmegen, surpervised by Bas Spitters and Freek Wiedijk. [blog post] [report] [slides (fr)] - L3 (2013):
*Streaming string transducers*at LaBRI, Bordeaux, supervised by Anca Muscholl and Sylvain Salvati. [report] [slides (fr)]

- 2017: Practical sessions at École Polytechnique:
*Introduction à l'informatique*(INF311).*Concurrence*(INF431).

- 2016: Computer-Aided Formal Reasoning (LMU Munich)

- A presentation of λ-calculus in terms of alligators.
- A cartoon proof of Löb's theorem.
- A self-referential multiple choice test by Jim Propp.
- The blue-eyed logicians puzzle.
- The hydra game (blog post by Andrej Bauer).
- Research paper generators: maths and computer science.
- Électronique Digérateur Science 2000+ (†)
- Webcomics I enjoy : xkcd, smbc and the rather silly adventures of Dr. McNinja.

(λxy. x.y@ens-lyon.fr) jeremy ledent