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.
LMSO: A Curry-Howard Approach to Church’s Synthesis via Linear Logic
with Colin Riba
Accepted at LICS 2018
A Curry-Howard Approach to Church's Synthesis
with Colin Riba
The Logical Strength of Büchi's Decidability Theorem
with Leszek Aleksander Kołodziejczyk, Michał Skrzypczak and Henryk Michalewski
Some formalizations in Coq I made as a hobby.
Cantor-Bernstein is classical
with Chad Brown
A proof that the Cantor-Bernstein theorem implies excluded middle as soon as P(ℕ) exists (this fails in topos lacking a natural number object). This is formalized in MLTT + functional extensionality, where we show that CB implies excluded middle (for hProps).
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.