# Presentation

Welcome to my research page.

I'm a PhD student at Univ. Paris Saclay and Univ. Paris under the supervision of Benoît Valiron and Alexis Saurin

# Research Interest

I'm currently working on the relation between Linear Logic and Quantum Computation. I'm aiming at developing 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**WIP**has been published at RC 2020, but beware as they are a few mistake in it that will be corrected in the final work.

Aside from that I'm also working on two sub-project :

The first one is on the relation between the ZX Calculus and Proof Net by the use of Geometry of Interaction. I'm working on this with Renaud Vilmart and Benoît Valiron and Marc de Visme. A first paper has been published at MFCS 2021.

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.

I'm also interested (even if I'm not working on it) on those subjects and would love to explore them at some point :

- 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 :**kostia@{lri, irif}.fr**