I am a PhD student at ENS Lyon and at the University of Warsaw since September 2016, under the
supervision of Colin Riba and Henryk Michalewski.
My current work focuses on the constructive aspects of Monadic Second Order logic.
I am generally interested in topics around logic, realizability, automata theory
and type theory.
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, pdf
The Logical Strength of Büchi's Decidability Theorem, with Leszek Aleksander Kołodziejczyk, Henryk Michalewski and Michał Skrzypczak, CSL 2016, pdf
Integrating Linear and Dependent Types, with Nick Benton and Neel Krishnaswami, POPL 2015, pdf source code
Cantor-Bernstein implies Excluded Middle, with Chad E. Brown, pdf formalization in Coq
Some formalizations in Coq I made as a hobby.
Ramsey's theorem via H-well-foundedness
A formalization of Stefano Berardi and Silvia Steila's paper
An intuitionistic version of Ramsey's Theorem and its use in Program Termination,
exhibiting a theorem analogous to the infinite Ramsey theorem admitting a constructive proof.
The paper introduces the notion of H-well-foundedness for relations, generalizing well-foundedness.
Their main theorem state that this notion is stable under finite union, which leads them to a second
constructive proof of Podelski and Rybalchenko's Termination Theorem.
- An equational theory for Mealy machines link
A little combinator language for letter-to-letter transducers together with a complete equational theory.
This essentially come from the remark that all such transducers correspond to the class of functions between
streams including lifting of maps between alphabets and closed by composition and parametric guarded fixpoints.