QCOMICAL School 2025

on Quantum and Classical Programming Languages and Semantics

The first QCOMICAL School will take place in Nancy, France, in 2025 as part of the QCOMICAL project. The school will offer tutorials and lectures by leading researchers involved in the project, working on quantum computing as well as related topics in programming languages and semantics, fostering interaction across foundational approaches.

November 3 to 7, 2025 – Nancy, France

Courses and Lecturers

Course titles are tentative and indicate the general subject areas to be covered.

• Tutorial: Introduction to Quantum Computing — Simon Perdrix (Inria/LORIA)

  Abstract: In this course, I will provide an introduction to quantum computing. We will cover the fundamental postulates underlying quantum computing and review a selection of quantum algorithms. Additionally, I will briefly outline the main challenges faced by the field.

• Tutorial: Introduction to ZX Calculus — Miriam Backens (Inria/LORIA)

  Abstract: The ZX-calculus is a graphical formalism for reasoning about quantum computing which is more flexible than quantum circuits, making it both intuitive and performant. Its applications include optimisation and classical simulation of quantum computations, translation between circuit-based and measurement-based models of quantum computation, design and analysis of quantum error-correcting codes, and more. This tutorial will present the core ZX-calculus with its complete equational theory, and show examples. It will also give an overview over different variants of the ZX-calculus and their uses.

• Quantum Programming Languages — Benoît Valiron (CentraleSupélec)

  Abstract: This course will present the specificities of quantum programming langugages. In particular, we shall discuss: the interaction with the quantum co-processor ; dedicated type-systems ; classical versus quantum control.

• Quantum Linear Optics — Timothée Goubault de Brugière (Quandela)

  Abstract: Linear optics stand as an alternative way to perform quantum computations, with its own rules. In this course we introduce the basic concepts of linear optics, how to classically simulate and compile linear optical system. We also show how to reproduce standard qubit-based paradigms such as quantum circuits or MBQC.

• Realisability — Emmanuel Beffara (Université de Grenoble)

  Abstract: The core idea of realisability is to connect an abstract computational model with a logical language through the concept of realisation, which semantically defines what it means for an object to serve as a witness for a statement. Over time, many variations of this principle have been developed, linking diverse formal programming languages with different logics. These applications demonstrate the method’s power in achieving results such as proving logical consistency, ensuring the correct behavior of typed programs, and extracting certified programs from proofs.
  
  The course will cover this methodological framework and its applications to intuitionistic, classical, and linear logics. We will also explore the program of algebraisation of realisability, which seeks to unify the semantics of provability and proofs within a consistent axiomatic framework. A particular focus will be the foundational challenges of realisability for concurrent models of computation, a key objective of Work Package 3 in the QComical project.

• Concurrency — Michele Pinna (Università degli Studi di Cagliari)

  Abstract: The purpose of the course is to provide a broad overview of some fundamental models of distributed computation studied in theoretical computer science. These models take the form of mathematical formalisms for describing and reasoning about the behaviour of concurrent systems. Their role is twofold: on the one hand, to deepen our theoretical understanding of such systems and their behaviour; on the other hand, to support practical methods for their design and analysis. Throughout the lessons, we will highlight key differences between the models and explore their interrelationships.

• Quantitative Types — Pablo Barenbaum (UNQ (CONICET) & UBA)

  Abstract: Intersection type systems are type systems for lambda-calculi that incorporate a type constructor A∩B. Intersection is a form of polymorphism: a term t can be assigned an intersection type A∩B whenever it behaves both as a term of type A and as a term of type B. One interesting aspect of these systems is that they can be used to characterise notions of normalisation. For example, a term is typable in Coppo and Dezani's system if and only if it is strongly normalising.
  
  More recently, non-idempotent intersection type systems have been introduced. These systems incorporate an intersection type constructor A∩B which is not idempotent, i.e. A∩A and A are not equivalent. Non-idempotent intersection is akin to multiplicative conjunction (A⊗B) in Linear Logic. This intuitively means that terms can be understood as resources, and that each subterm must be typed as many times as it is going to be used in a reduction to normal form.
  
  Just as in the idempotent case, the existence of a typing derivation can be used to obtain qualitative information about the behaviour of a program (such as termination). The interesting difference is that typing derivations in systems with non-idempotent intersection also provide *quantitative* information about the behaviour of a program (such as the length of the reduction to normal form). These systems usually provide quantitative upper bounds. It is possible to refine them to be "tight", i.e. to provide exact quantitative measures.
  
  In this course, we will study how quantitative type systems can be designed to capture notions of normalisation (head, weak, and strong normalisation), to provide upper bounds, and how they can be refined to obtain exact bounds. We will also mention some applications, and in particular, normalisation of reduction strategies and observational equivalence of calculi.

Schedule

Below is the preliminary schedule scheme:

Registration

Registration is now closed. For those registered, participation is free of charge. Coffee breaks and lunches will be provided.

Venue

Visa Information

Organisers

• Kostia Chardonnet - Inria/LORIA
• Alejandro Díaz-Caro (Chair) - Inria/LORIA & UNQ - Contact
• Simon Perdrix - Inria/LORIA
• Benoît Valiron - CentraleSupélec

Sponsors

Diamond



Gold



Silver





Hosted by the Centre Inria de l'Université de Lorraine



MSCA Staff Exchanges — Funded by the European Commission through Marie Skłodowska-Curie Actions – Staff Exchanges