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.

## Publications

*LMSO: A Curry-Howard Approach to Church’s Synthesis via Linear Logic*

with Colin Riba

Accepted at 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, Michał Skrzypczak and Henryk Michalewski

CSL 2016

pdf

*Integrating Linear and Dependent Types*

with Nick Benton and Neel Krishnaswami

POPL 2015

pdf source code

## 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 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
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.

firstname.lastname@ens-lyon.fr