Presentation
Welcome to my research page.
I'm a post-doc at Inria Nancy in the MOCQUA
team, working with Simon Perdrix.
Before that, I was doing a post-doc at Dipartimento di
Informatica at the University of Bologna, Italy,
under the supervision of Ugo Dal Lago
I did my PhD at Univ. Paris Saclay and Univ.
Paris under the supervision of Pablo Arrighi and
Benoît Valiron
and Alexis
Saurin.
I defended my PhD on the 9 of January 2023, you can
find my manuscrit here and the slides
of my defense here
Research Interest
I'm currently working on the relation between Linear Logic and Quantum Computation. The topic of my PhD was to develop a Curry-Howard correspondence for pure quantum computation with rich type system (induction and co-induction). This also means handling recursion for pure quantum computation, which is believed not to be meaningful in its most general form. A first paper towards this direction has been published at CSL 2023 in the context of classical, linear and reversible computation (a subcase of quantum computation). I'm also working on quantum control for quantum computation, through graphical languages. This work was initialy done with the use of Token-Based semantics, inspired from the Geometry of Interaction . This has led to a first work on the ZX-Calculus which was published at MFCS 2021 with Benoît Valiron and Renaud Vilmart. This line of work has now led to the developed of a new graphical language for quantum computation with quantum control, called the Many-Worlds Calculus, in collaboration with Bnoît Valiron, Renaud Vilmart and Marc de Visme where a draft is available on HAL and Arxiv. I'm also working with Louis Lemonnier and Benoît Valiron and Robin Kaarsgaard on the semantic of reversible languages and quantum languages. A first paper has been published at MFPS 2021. My (non-exhaustive) lists of topics I'm interested in:- Correctness Criterion for Proof Nets
- String Diagrams for Quantum Computing
- Transcendental Syntax
- Evaluation strategies of lambda-calculus
- Classical and quantum extension of lambda-calculus
- Dependent type theory and Intersection Types
- Homotopy Type Theory
- Proof Assistant (in particular Coq)
- Semantic of programming languages