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
• 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

Contact

You can contact me at : [first name].[last name]@pm.me

Important Stuff

Nothing matters.