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

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

Some formalizations in Coq I made as a hobby.

Cantor-Bernstein is classical link

with Chad Brown

A proof that the Cantor-Bernstein theorem implies excluded middle as soon as P(ℕ) exists (this may fail in a 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 link

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.

2018

- TD FDI:
TD 1
TD 2
TD 3
TD 4
TD 5
TD 6
TD 7
TD 8
TD 9
TD 10
DM 2
TD 11
TD 12

Correction DM 2 (suggestion de présentation) - TP LIFAP3
- TP LIFASR3

firstname.lastname@ens-lyon.fr