I am currently working as a postdoc in the MSP Group at the University of Strathclyde (Glasgow).

I work on a categorical approach to game theory, based on the notion of *Open Games*.

I recently finished my PhD at École Polytechnique, supervised by Éric Goubault and Samuel Mimram.

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

[9] |
Robert Atkey, Bruno Gavranović, Neil Ghani, Clemens Kupke, Jérémy
Ledent, and Fredrik Nordvall Forsberg.
Compositional game theory, compositionally, ACT 2020.
[ |
slides |
pdf ]
We present a new compositional approach to Compositional Game Theory based upon the notion of arrows, a concept originally from functional programming. We model equilibria as a module over an arrow and define an operator to build a new arrow from such a module over an existing arrow. We also model strategies as graded arrows and define an operator which builds a new arrow by taking the colimit of a graded arrow. We use this compositional approach to CGT to show how known and previously unknown variants of open games can be proven to form symmetric monoidal categories. |

[8] |
Hans van Ditmarsch, Eric Goubault, Jérémy Ledent, and Sergio
Rajsbaum.
Knowledge and simplicial complexes, 2020.
[ |
bib |
url |
pdf ]
Simplicial complexes are a versatile and convenient paradigm on which to buildall the tools and techniques of epistemic logic. Thus, we can define: knowledge, belief, bisimulation, the group notions of mutual, distributed and common knowledge, and also dynamics in the shape of simplicial action models. We give a survey on how to interpret all such notions on simplicial complexes. |

[7] |
Jérémy Ledent and Samuel Mimram.
A sound foundation for the topological approach to task solvability.
In 30th International Conference on Concurrency Theory, CONCUR
2019.
[ |
bib |
DOI |
slides |
pdf ]
The area of fault-tolerant distributed computability is concerned with the solvability of decision tasks in various computational models where the processes might crash. A very successful approach to prove impossibility results in this context is that of combinatorial topology, started by Herlihy and Shavit in 1999. However, their so-called Asynchronous Computability Theorem was only proved in the context of processes communicating through read-write registers. In this paper, we prove a generalization of this theorem that applies to any kind of shared object. |

[6] |
Éric Goubault, Marijana Lazic, Jérémy Ledent, and Sergio
Rajsbaum.
A dynamic epistemic logic analysis of the equality negation task.
In Dynamic Logic. New Trends and Applications - Second
International Workshop, DaLí 2019.
[ |
bib |
DOI |
long version |
pdf ]
In this paper we study the solvability of the equality negation task in a simple wait-free model where processes communicate by reading and writing shared variables or exchanging messages. In this task, two processes start with a private input value in the set {0, 1, 2}, and after communicating, each one must decide a binary output value, so that the outputs of the processes are the same if and only if the input values of the processes are different. This task is already known to be unsolvable; our goal here is to prove this result using the Dynamic Epistemic Logic approach introduced in a previous paper. We show that in fact, there is no epistemic logic formula that explains why the task is unsolvable. We fix this issue by extending the language of our DEL framework using so-called DEL with factual change. |

[5] |
Éric Goubault, Marijana Lazic, Jérémy Ledent, and Sergio
Rajsbaum.
Wait-free solvability of equality negation tasks.
In 33rd International Symposium on Distributed Computing, DISC
2019.
[ |
bib |
DOI |
slides |
pdf ]
We introduce a family of tasks for n processes, as a generalization of the two-process equality negation task of Lo and Hadzilacos. We study the solvability of these tasks using techniques from combinatorial topology. |

[4] |
Éric Goubault, Jérémy Ledent, and Samuel Mimram.
Concurrent specifications beyond linearizability.
In 22nd International Conference on Principles of Distributed
Systems, OPODIS 2018.
[ |
bib |
DOI |
slides |
pdf ]
A very general way to specify concurrent objects is to simply give the set of all the execution traces that we consider correct for the object. In many cases, one is only interested in studying a subclass of these concurrent specifications, and more convenient tools such as linearizability can be used to describe them. In this paper, what we call a concurrent specification will be a set of execution traces that moreover satisfies a number of axioms. As we argue, these are actually the only concurrent specifications of interest. Restricting to this class of concurrent specifications allows us to derive a Galois connection theorem relating different variants of linearizability. |

[3] |
Éric Goubault, Jérémy Ledent, and Samuel Mimram.
Brief announcement: On the impossibility of detecting concurrency.
In 32nd International Symposium on Distributed Computing, DISC
2018.
[ |
bib |
DOI |
pdf ]
We identify a general principle of distributed computing: one cannot force two processes running in parallel to see each other. This principle is formally stated in the context of asynchronous processes communicating through shared objects, using trace-based semantics. We prove that it holds in a reasonable computational model, and then study the class of concurrent specifications which satisfy this property. |

[2] |
Éric Goubault, Jérémy Ledent, and Sergio Rajsbaum.
A simplicial complex model for dynamic epistemic logic to study
distributed task computability.
In Proceedings Ninth International Symposium on Games, Automata,
Logics, and Formal Verification, GandALF 2018.
[ |
bib |
DOI |
slides |
long version |
pdf ]
The usual epistemic model for a multi-agent system is based on a Kripke frame, which is a graph whose edges are labeled with agents that do not distinguish between two states. We propose to uncover the higher-dimensional information implicit in this structure, by introducing a topological notion of model based on simplicial complexes. We then use Dynamic Epistemic Logic to study how a simplicial model changes after a set of agents communicate with each other. We thus provide a bridge between DEL and the topological theory of distributed computability, which studies task solvability in a shared memory or message passing architecture. |

[1] |
Martin Hofmann and Jérémy Ledent.
A cartesian-closed category for higher-order model checking.
In 32nd Annual ACM/IEEE Symposium on Logic in Computer
Science, LICS 2017.
[ |
bib |
DOI |
slides |
pdf ]
In previous work, the construction of an abstract lattice from a given Büchi automaton is described. This abstract lattice is finite and allows one to decide whether finite and infinite traces of first-order recursive boolean programs are accepted by the automaton. In this paper, we show how to derive from the abstract lattice a cartesian-closed category with fixpoint operator in such a way that the interpretation of a higher-order recursive program yields precisely the abstraction of its set of finite and infinite traces. Thus, this provides a new algorithm for the higher-order model checking problem for trace properties, by simply evaluating the semantics of a program in our model. |

*Geometric Semantics for Asynchronous Computability (2019)* [ manuscript | slides ]

- 2016: internship at Ludwig-Maximilians University (LMU), Munich, supervised by Martin Hofmann.
*Higher-order model checking of Büchi properties.*[ LICS'17 paper | 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) ]

- 2016-2019: Practical sessions at École Polytechnique:
*Introduction to formal languages*(CSE206).*Mécanismes de la programmation orientée-objet*(INF371).*Les bases de la programmation et de l'algorithmique*(INF411).*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.
- Webcomics I enjoy : xkcd, smbc and the rather silly adventures of Dr. McNinja.

(λxy. x.y@strath.ac.uk) jeremy ledent