Research
Research
My publications grouped by theme. See my DBLP entry for a chronological list.
Axiomatizing graph isomorphism
For every positive integer k, there is a syntax generating all graphs of treewidth k. However two distinct terms of this syntax may denote the same (isomorphic) graph. With Damien Pous and Samuel Humeau, we consider the following question: is there a finite set of axioms, from which we can derive all equalities between terms denoting isomorphic graphs? We call this question the problem of axiomatizing graph isomorphism.
Regular expressions for graph languages of bounded treewidth
In the following paper, I propose a syntax of regular expressions, which describes languages of treewidth 2 graphs. These languages correspond exactly to those languages of treewidth 2 graphs, definable in the counting monadic second-order logic (CMSO).
Regular expressions for treewidth 2 graphs.
My current goal is to generalize these expressions to graph languages of bounded treewidth.
Regular expressions for tree transducers
In this joint work with Mikolaj Bojanczyck, we decompose first-order tree-to-tree transuctions into basic blocs.
Kleene and Relation algebra
What are the laws ruling relations? Can we decide if a law is valid for all relations? Can we finitely axiomatize these laws? These are the questions we try to answer in the following series of papers.
Kleene Algebra with Hypotheses. With Denis Kuperberg, Damien Pous and Pierre Pradic.
Left-Handed Completeness via Cyclic Proofs. With Anupam Das and Damien Pous.
Completeness for Identity-free Kleene Lattices. With Damien Pous.
Cyclic proofs
Cyclic proof are those mathematical demonstrations where we are allowed to use the statement to be proved as a hypothesis of the proof. Without any further constraints, these proofs would be unsound, as we can prove false like this. However, when they satisfy a certain validity condition, they become genuine proofs. They are in fact widely used in the context of fixed point logics.
​
With Alexis Saurin and David Baelde, we contributed to set the proof-theoretical foundations of cyclic proofs, by showing that they enjoy the properties of cut elimination and focalization in the following paper. More material can be found in PhD thesis below.
Using cyclic proofs, we obtain in the following papers, a constructive completeness proof for the linear-time µ-calculus w.r.t. Kozen’s axiomatization. Part of this work was made jointly with Alexis Saurin, David Baelde and Lucas Hirsh.
With Alexis Saurin, David Daelde and Denis Kuperberg, we extended the validity condition to capture more proofs, via what we call bouncing threads.
Linear Logic
In this joint work with David Baelde and Alexis Saurin, we propose a semantics of linear Logic with fixed points in the framework of ludics, which is very close to game semantics.
In the following paper, we provide a new correctness criterion for MLL proof nets. This is a joint work with Alexis Saurin and Marc Bagnol.