Spring School 2026

TBA

Course Title:
Compilation and Resource Estimation

Abstract:
Recent advances in quantum hardware provide increasing evidence that future quantum computers will be capable of running fault-tolerant algorithms. However, fault-tolerance incurs a resource overhead and understanding the true cost of an algorithm, beyond its promised computational complexity, is critical for practical implementations. This module is an overview of fault-tolerant resource estimation from a quantum software and compilation perspective. Starting from a high-level problem description, we will compile and optimise a quantum program down to the physical level. We will take a hands-on approach and explore how hardware assumptions and design decisions across the software stack impact both resource estimates and their interpretation by researchers and policy makers.

Course Title:
Causality in Quantum Theory from Within

Abstract:
This course will cover  the path integral in quantum mechanics. The path integral approach to quantum foundations as a stand-alone alternative to the canonical framework. The path integral approach is  based on concepts of history, event and event algebra, quantum measure and decoherence functional.

The recovery of Hilbert space from the path integral approach. A novel proposal for an intrinsic causality condition that is internal to a path integral quantum theory and that does not rely on any external measurement or agent. 

Course Title:
Quantum Error Correction

Abstract:
Quantum error correction, and more broadly fault-tolerance theory, addresses how computation can be carried out in the presence of noise. Building on a light mathematical background, we will outline the desiderata of a fault-tolerant protocol and highlight some of the reasons why these desiderata are hard to satisfy in practice. We will then zoom in on two especially active areas of the field: logic, meaning how to perform computation once quantum information is protected by an error-correcting code, and decoding, the classical counterpart of any fault-tolerant protocol. So what is it, precisely, that makes reliable quantum computation possible, and why is it difficult to achieve?

Course Title:
Quantum Programming Languages

Abstract:
In this course, we shall analyse the structure of quantum algorithms, and what programming constructs make sense to code them up. We shall review the existing quantum programming paradigms, and discuss type systems and semantics.

Course Title:
Semantics of Mixed Quantum Theory

Abstract:
Our exploration of semantics of mixed quantum theory will start with linear logic and its connections to quantum mechanics. Once we introduce ourselves to the basics of linear logic, we pick up the lens of  category theory and aim it at the logic. What we see through the lens will be semantics of linear logic — however in different shades. We call them monoidal categories, compact closed categories, linearly distributive categories, and so on. Why are we interested in studying categorical semantics (vernacular) of linear logic? It is because we can then draw pictures instead of writing long complex proofs using symbols. We will explore these pictorial languages while making our way steadily towards utilizing them as a vernacular for quantum theory.

While linear logic provides a base vernacular for quantum theory, we need another ingredient to make its semantics quantum-ready. This is called a dagger functor which will allow us to talk about “quantum observables”.  Different semantics of linear logic come with different advantages — dagger compact closed categories well-suited to model finite-dimensional quantum systems while infinite-dimensional systems need the full power of linear logic, so one moves to dagger linearly distributive categories. While these semantics are a blueprint (think of it as a grammar), we will pick a few concrete forms of these blueprints — like the Hilbert spaces and the finiteness spaces — to witness ‘quantumness’ like complete positivity, complementarity, and measurement.

Towards the end of the journey, we shall make a bold attempt to amalgamate the semantics of concurrency and the semantics of quantum theory since they both spring from the common ground of linear logic. For this, we shall take aid in a functional concurrent programming language called CaMPL.

If you would like to prepare yourself for this journey, I would recommend reading a couple of posts in https://lineardistributivity.org/  and if you are programmer, https://campl-ucalgary.github.io/ is another fun site to explore.

Keywords: Linear logic, dagger compact closed categories, dagger linearly distributive categories, pictorial calculus, completely positive maps, complementarity, concurrency, quantum concurrency.