==== Gaëtan LOPEZ ==== 

1st year PhD in Computer Science at IRIF, supervised by [[https://www.irif.fr/~gio/index.xhtml|Giovanni Bernardi]], co-supervised by [[https://hugo.feree.fr//|Hugo Férée]]. 

== Contact == 

|Email   |  gaetan.lopez@irif.fr  |
|Office  |  4059  |


My research interests include :

  * Quantum Computation

  * Quantum Information

  * Lambda calculus

  * Process Calculus

==== Publications and Preprints ==== 
== A Rewriting Theory for Quantum Lambda-Calculus == 

Joint work with [[https://www.irif.fr/~faggian/|Claudia Faggian]] and [[https://www.monoidal.net/|Benoît Valiron]].

//33rd EACSL Annual Conference on Computer Science Logic 2025 [[https://csl2025.github.io/|(CSL)]], 10-14 February 2025//

[[https://arxiv.org/abs/2411.14856|[arXiv, 2024]]]

Presentation on slides : {{ :users:glopez:a_rewriting_theory_on_q-lambda_calculus.pdf | [PDF]}}

==== Internships ==== 


== CCS and the harmony lemma in COQ ==

Supervised by [[https://www.irif.fr/~gio/index.xhtml|Giovanni Bernardi]] and [[https://hugo.feree.fr//|Hugo Férée]].

Formalization in COQ of Calculus of Communicating Systems, Calculus of Communicating Systems with Value Passing, Calculus of Communicating Systems with Sequenciation.

Formalization in COQ of their Harmony Lemmas.

Report : {{ :users:glopez:coq_can_communicate.pdf | [PDF]}}

== Quantum Lambda-Calculus with measurement == 

Supervised by [[https://www.irif.fr/~faggian/|Claudia Faggian]] and [[https://www.monoidal.net/|Benoît Valiron]].

Developping confluence and normalization on a quantum lambda calculus with measurement.

Report : {{ :users:glopez:quantum_lambda_calculus.pdf | [PDF]}}