QCOMICAL School 2026

on Quantum Programming Languages and Semantics

After a succesfull first edition in Nancy (France), the second QCOMICAL School will take place in Pisa (Italy) as part of the QCOMICAL project. The school will offer tutorials and lectures by leading researchers involved in the project, working on quantum computing with a focus on quantum programming languages and their semantics, fostering interaction across foundational approaches.

November 16 to 20, 2026 – Pisa, Italy

Courses and Lecturers

• Computational Quantum Logic - Alejandro Díaz-Caro (Inria Nancy, France & Universidad de la República, Uruguay)

  In this course, we will explore the logical foundations of quantum computing through the lens of the Curry-Howard correspondence. We will look at both directions of this relationship: how linear logic provides a natural framework for quantum mechanics, and conversely, what kind of logic emerges when we take quantum linearity as the starting point. Along the way, we will explore the challenges posed by measurement and the resulting non-determinism, examining different approaches to incorporating non-deterministic choice into logical systems.

• Bayesian Networks (and Quantum Ones) Claudia Faggian (IRIF/CNRS, France)

  Quantum theory can be framed as a theory of inference. What it predicts are the probabilities of measurement outcomes on a system; so framed, prediction is a problem of probabilistic inference. It is then natural to ask if and how the tools developed for classical Bayesian inference carry over to the quantum setting — an active research area. The first part of the course introduces Bayesian networks, prominent graphical models for probabilistic reasoning under uncertainty, which have a dual nature as tools for inference and as causal models. We present their semantics and the basic mechanisms of inference. The second part opens towards quantum Bayesian networks, which extend the framework to systems involving both classical and quantum data. The Bell experiment — Alice and Bob measuring a pair of entangled qubits in laboratories far apart — will be our guiding example.

• Quantum Process Calculi Fabio Gadducci (CINI/Università di Pisa, Italy) & Gabriele Tedeschi (IRIF/CNRS, France)

  Whereas most quantum protocols are described in natural language and rarely analysed through the lens of formal methods, modern quantum network infrastructures demand rigorous guarantees of correctness and security. Process calculi represent a natural candidate for quantum protocol verification, given their effectiveness in modelling and analysing distributed systems. This course introduces the lqCCS language, a quantum extension of value-passing CCS. It describes its operational semantics, illustrates the associated testing and bisimulation equivalences, and provides examples of protocol specifications to assess the calculus' adequacy in proving their correctness.

• Tool Session: Automated Verification of Quantum Protocols Giuseppe Lomurno (Università di Pisa, Italy)

  Quantum communication is moving from laboratory demonstrations to deployed security applications, so the correctness of quantum protocols is becoming a practical concern rather than a theoretical one. Verification is hard on multiple axis: the systems act on possibly large quantum states with probabilistic behaviour, and being concurrent, they also exhibit non-deterministic behaviour. These two features do not compose for free: theoretical work shows that naively extending classical techniques breaks soundness, and that scheduling must be handled with care. We present an interactive workbench that implements these results. Protocols are written in lqCCS, a process algebra that adds quantum operations to the simple syntax of CCS. The tool typechecks protocols and sepcifications, derives their semantics as labelled transition systems, and decides behavioural equivalence via bisimilarity, both from the command line and through a GUI in which the state space can be explored interactively.

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

  In this lecture, we will discuss what it means to program quantum computers: what is the computational model, what is the general structure of quantum algorithms, and what it implies in terms of programming structures and constraints. We shall in particular focus on the functional paradigm, and the differences with the classical framework.

• Categories for Quantum Computing Vladimir Zamdzhiev (INRIA/Université Paris Saclay, France)

  In this course we recall some of the more important categories that have been studied in the program of Categorical Quantum Mechanics (CQM) for finite-dimensional quantum systems. Examples include the category FHilb of finite-dimensional Hilbert spaces and linear maps between them and a category that is equivalent to finite-dimensional C*-algebras and completely positive (CP) maps between them. We then consider additional categories that are relevant for quantum computation where we take into account normalisation constraints and show that we still have nice categorical structures that are compatible with the Heisenberg-Schrödinger duality of quantum theory. The latter results are based on a joint paper with Thea Li and other papers coauthored with Bert Lindenhovius.

Registration

Venue

Visa Information

Organisers

• Roberto Bruni - University of Pisa, Italy
• Alejandro Dìaz-Caro - Inria Nancy, France & Universidad de la República, Uruguay
• Fabio Gadducci (chair) - University of Pisa, Italy - Contact
• Gabriele Tedeschi - IRIF, France - Contact
• Benoît Valiron - CentraleSupélec, France

Sponsors

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