I am a lecturer at Swansea University since fall 2021. I am generally interested in topics around logic, realizability, automata theory and type theory.

Before that, I was a doctoral student at ENS Lyon and at the University of Warsaw, under the supervision of Colin Riba and Henryk Michalewski, and went on to be a postdoc for two years at the university of Oxford, working with Michael Benedikt. My thesis focused on the constructive aspects of Monadic Second Order logic.


Comparison-free polyregular functions, with Lê Thành Dũng Nguyễn and Camille Noûs, ICALP 2021, pdf
Generating collection queries from proofs, with Michael Benedikt, POPL 2021, pdf
Implicit automata in typed λ-calculi I: aperiodicity in a non-commutative logic, with Lê Thành Dũng Nguyễn, ICALP 2020, pdf
From normal functors to logarithmic space queries, with Lê Thành Dũng Nguyễn, ICALP 2019, pdf
Kleene Algebra with Hypotheses, with Amina Doumane, Denis Kuperberg and Damien Pous, FOSSACS 2019, pdf
A Dialectica-Like Interpretation of a Linear MSO on Infinite Words, with Colin Riba, FOSSACS 2019, pdf
LMSO: A Curry-Howard Approach to Church’s Synthesis via Linear Logic, with Colin Riba, LICS 2018, pdf
A Curry-Howard Approach to Church's Synthesis, with Colin Riba, FSCD 2017/LMCS 2019, pdf
The Logical Strength of Büchi's Decidability Theorem, with Leszek Aleksander Kołodziejczyk, Henryk Michalewski and Michał Skrzypczak, CSL 2016/LMCS 2019, pdf
Integrating Linear and Dependent Types, with Nick Benton and Neel Krishnaswami, POPL 2015, pdf source code


Implicit automata in typed λ-calculi II: streaming transducers vs categorical semantics, with Lê Thành Dũng Nguyễn and Camille Noûs, pdf
Cantor-Bernstein implies Excluded Middle, with Chad E. Brown, pdf formalization in Coq


Here are a couple slides from talks I have given: PhD defense (23/06/20), Implicit automata in λ-calculi (I) (24/06/20, Warsaw automata webinar), Implicit definitions of nested collections (06/11/20, Birmingham theory webinar, 04/12/20 seminar of the LINKS team (Lille)), Implicit automata in λ-calculi (II) (16/12/20, IRIF gt réalisabilité, 05/02/21, Journées LHC, 08/03/21, GdT plume, 28/06/21, Structure meets Power workshop (abstract)), Logical complexity of MSO over countable linear orders (17/02/21, Manchester logic seminar), Implicit automata in λ-calculi (I.5) (19/03/21, IRIF gt automate), Comparison-free polyregular functions (ICALP21)


Some things I formalized in Coq.