# 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 formAside from that I'm also working on multiple 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.

I'm also working on adapting the result of multifocusing and proof net in Chapter 10 of Alexis Saurin thesis for additive proof net and proof net for infinitary linear logic. I'm working on this with Abhishek De and Alexis Saurin.

Finally, I'm working on translation Boolean Circuits to Quantum Circuits with the use of Proof Nets, and hope to find some result in complexity theory. I'm working on this with Ugo Dal Lago.

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

# Important Stuff

# Contact

You can contact me at :**kostia@{lri, irif}.fr**