- First-order tree functions. In preparation. Joint work with Mikołaj Bojańczyk.
- Axiomatizing Kleene algebras with uninterpreted function symbols. In preparation. Joint work with Damien Pous.
- Bouncing threads for infinitary and circular proofs. Submitted. Joint work with David Baelde, Denis Kuperberg and Alexis Saurin.
- Kleene algebras with hypothesis. FOSSACS 2019. Joint work with Damien Pous, Denis Kuperberg and Pierre Pradic.
- Left Handed Completeness via cyclic proofs. LPAR 2018, Awassa. Joint work with Anupam Das and Damien Pous.
- Completeness for Identity-free Kleene Lattices. CONCUR 2018, Beijing. Joint work with Damien Pous.
- Constructive completeness for the linear-time mu-calculus. LICS 2017, Reykjavik. Kleene Award 2017.
- Infinitary Proof Theory: the Multiplicative Additive Case. CSL 2016, Marseille. Joint work with David Baelde and Damien Pous.
- Towards completeness via proof seach in the linear time mu-calculus. LICS 2016, New York. Joint work with David Baelde, Lucca Hirshi and Alexis Saurin.
- Least and greatest fixed points in Ludics. CSL 2015, Berlin. Joint work with David Baelde and Alexis Saurin.
- On the dependencies of logical rules. FOSSACS 2015, London. Joint work with Marc Bagnol and Alexis Saurin.
Thesis