QUASAR: Quantum Semantics and Reasoning

• MOCQUA project-team, Centre Inria de l’Université de Lorraine, Inria (France)
• QUACS project-team, Inria Saclay Centre, Inria (France)
• GALLINETTE project-team, Inria Centre at Rennes University, Inria (France)
• Universidad de Chile (Chile)
• Universidad de la República (Uruguay)
• Institut de Mathématiques de Marseille (I2M) (France)
• Laboratoire d'Informatique de Grenoble (LIG) (France)
• Universidad de Los Andes (Colombia)

This project aims to develop theoretical foundations for quantum programming languages and reasoning tools, integrating logics, type systems, and categorical semantics. Building on prior work from the Lambda-S calculus, the Sup-calculus and the ZX-calculus, and aligned with the ongoing QCOMICAL consortium, the project will study new structures for quantum programs that combine expressiveness, correctness, and compositionality.

We will explore logical and semantic frameworks that account for the unique phenomena of quantum computation from both operational and denotational perspectives. Our approach emphasises the use of category theory as a unifying language for quantum semantics, and proof assistants (such as Rocq/Coq) as a platform for verification and reasoning.

The project brings together partners from France, Chile, Uruguay, and Colombia, combining expertise in quantum programming, formal semantics, proof theory, and quantum physics. It will support training of young researchers, international missions of researchers, joint publications, and intercontinental collaboration, fostering long-term cooperation across the South America-Europe axis.

In France: 

• Pablo Arrighi, researcher, QUACS project-team, Inria Saclay Centre, Inria
• Kathleen Barsse, PhD student, MOCQUA project-team, Centre Inria de l’Université de Lorraine, Inria
• Emmanuel Beffara, researcher, QUASAR coordinator, Laboratoire d'Informatique de Grenoble
• Colin Blake, PhD student, MOCQUA project-team, Centre Inria de l’Université de Lorraine, Inria
• Kostia Chardonnet, researcher, MOCQUA project-team, Centre Inria de l’Université de Lorraine, Inria
• Noé Delorme, PhD student, MOCQUA project-team, Centre Inria de l’Université de Lorraine, Inria
• Alejandro Díaz-Caro, researcher, QUASAR coordinator, MOCQUA project-team, Centre Inria de l’Université de Lorraine, Inria
• Antoine Guilmin-Crepon, PhD student, QUACS project-team, Inria Saclay Centre, Inria
• James Hefford, researcher, QUACS project-team, Inria Saclay Centre, Inria
• Julien Lamiroy, PhD student, QUACS project-team, Inria Saclay Centre, Inria
• Thea Li, PhD student, QUACS project-team, Inria Saclay Centre, Inria
• Octave Mestoudjian, PhD student, QUACS project-team, Inria Saclay Centre, Inria
• Étienne Miquey, researcher, QUASAR coordinator, Institut de Mathématiques de Marseille
• Romain Pechoux, researcher, MOCQUA project-team, Centre Inria de l’Université de Lorraine, Inria
• Simon Perdrix, researcher, MOCQUA project-team, Centre Inria de l’Université de Lorraine, Inria
• Nicolas Tabareau, researcher, GALLINETTE project-team, Inria Centre at Rennes University, Inria
• Benoît Valiron, researcher, QUACS project-team, Inria Saclay Centre, Inria
• Thomas Vinet, PhD student, MOCQUA project-team, Centre Inria de l’Université de Lorraine, Inria

In Chile: 

• Tomás Díaz, PhD student, Universidad de Chile
• Federico Olmedo, researcher, QUASAR coordinator, Universidad de Chile
• Gaspar Ricci, MSc student, Universidad de Chile
• Martín Segur, MSc student, Universidad de Chile
• Éric Tanter, researcher, Universidad de Chile

In Uruguay: 

• Mauricio Guillermo, researcher, Universidad de la República
• Malena Ivnisky, PhD student, Universidad de la República
• Octavio Malherbe, researcher, QUASAR coordinator, Universidad de la República
• Nicolás Monzón, MSc student, Universidad de la República
• Alberto Pardo, researcher, Universidad de la República
• Julián Tricanico, MSc student, Universidad de la República
• Marcos Viera, researcher, Universidad de la República

In Colombia: 

• Julián David Calderón, PhD student, Universidad de Los Andes
• Andrés Reyes Lega, researcher, QUASAR coordinator, Universidad de Los Andes