Quantum Logic 2025-26

MEF - MSc in Physics Engineering

Dep. Informática, Universidade do Minho

Objectives and learning outcomes

The development of quantum information and computation entails the need for formal tools to model, verify and reason rigorously about quantum programs. This course explores

Thus, in the end, students will be able to apply to the development of quantum programs a solid and operative knowledge in program semantics and calculi.

Syllabus

Summaries (2025-26)

T Lectures
Feb 02 (16:00 - 18:00) Introduction to the course: motivation, objectives, learning outcomes, organisation. Introduction to the notion of a category and its relevance for Computer Science. Basic defintions and examples.
Feb 09 (16:00 - 18:00) Participação dos alunos na Jornadas de Física e Engenharia Física (por resposta a solicitação de dispensa de aulas).
Feb 16 (16:00 - 18:00) Further examples of categories. Notions of subcategory and dual category.
Feb 23 (16:00 - 18:00) Functors: definition, relevance and properties.
Mar 2 (16:00 - 18:00) Functors: examples. Introduction to universal properties. Initial and final object. Notion of product and coproduct. Examples.
Mar 16 (16:00 - 18:00) Natural transformations. Parametricity. Examples.

Categories as process theories. Introduction to diagramatic languages for monoidal categories and diagrammatic reasoning.

Mar 23 (16:00 - 18:00) Diagramatic languages for processes and diagrammatic reasoning. Relationship with monoidal categories. Circuits. States, effects and numbers. Examples.

Introduction to string diagrams. Separability. Process-state duality. Transposition.

Apr 13 (16:00 - 18:00) Conclusion of the previous lecture: Unitaries and projectors; Expressing quantum phenomena in string diagrams.

The process theory of linear maps.

Apr 20(16:00 - 18:00) The process theory of linear maps. Recovering Hilbert spaces from diagrams.
Apr 27 (16:00 - 18:00) Pure quantum processes and their theory. Process doubling.
May 04 (16:00 - 18:00) A case study: Programming quantum walks and reasoning about them in ZX.

TP Lectures
Feb 09 (09:00 - 11:00) Participação dos alunos na Jornadas de Física e Engenharia Física (por resposta a solicitação de dispensa de aulas).
Feb 16 (09:00 - 11:00) Recap of (dual) categories; definitions of inverse, monic and epic morphisms; discussions of Exercises 12, 14 and 16(i) of Lecture 1.
Introduction to string diagrams in category theory: boxes, wires, swaps. Example: the category of sets, together with morphisms: copy, delete, xor, and falsum (on bits).
Feb 23 (09:00 - 11:00) Recap of categories; Exercises 15 and 16(ii) of Lecture 1.
String diagrams: expressing and proving properties diagrammatically by means of our morphisms from last session (copy, delete, xor, falsum) together with negation.
Mar 2 (09:00 - 11:00) Recap of functors; Exercises 11 and 12 of Lecture 2.
Probabilistic computing in string diagrams: introduce probabilistic bitflips in the category of (real) vector spaces.
Mar 9 (09:00 - 11:00) Recap of products and coproducts; Exercises 13 and 14 of Lecture 3.
Probabilistic computing in string diagrams: universal copying (as universal arrow) versus our copy morphism (which copys a chosen basis); relation to probabilistic bitflips.
Mar 9 (16:00 - 18:00) Probabilistic computing: deterministic vs. probabilistic bit-operations in string diagrams.
Towards quantum computing: free Hilbet spaces as functor from Set to Hilb; translation of Bits and its operations (swap, copy, delete, xor, falsum, negation) to Hilb, preserving the properties from the first sessions.
Mar 16 (09:00 - 11:00) Exercise 6 of Lecture 3: coalgebras of functors.
Mar 23 (09:00 - 11:00) Exercise 9 of Lecture 5: naturality and symmetrie of braidings expressed in string diagrams.
Recap of our notions in classical, probabilistic and quantum computing. Missing ingredients of ZX-calculus: multiple in-and outputs of xor and copy map (via associativity); mirroring (via taking adjoints), leading to copy in different basis; Z and X gates as "quantum bitflips".
Homework: 1. show copy^dagger * dagger = id, for both copy maps (in X and Z basis). (Tip: abstract definition of adjoints)
2. describe Z and X-gates by brac-kets and deduce our interpretation as "quantum bit-flips". What's a fundamental difference to the probabilistic case? (Tip: consider the probabilistic bitflip with flipping proabilities p = 0.5 = q.)
3. try to vizualize (some of) our rules in zxlive, using the tools in "Start Derivation". (Remember that bitplips with phase alpha=0 are the identity)
Apr 7 (14:30 - 16:30) Discussion of projects for assignment.
Apr 20 (09:00 - 11:00) Discussion of homework from last session.
Towards ZX-calculus: definition of Z/X-spiders: using single-qbit Z/X-gates, our copy/xor morphisms, and their adjoints; graphical proof of spider fusion rule.
Apr 27 (09:00 - 11:00) Arriving at the ZX-calculus: proof and interpretation of remaining rules (pi commutation, copy 0/pi, Hadamard decomposition, color change);
Hands-on application in zxlive.
May 04 (09:00 - 11:00) Alternative ZX calculus editors ZX Sketch, ZX Calculator, ZXLab (with python package PyZX as underlying machinery).
From quantum cicuits to ZX-diagrams: translating the universal gate set {CNOT, H, Z(alpha)} to ZX diagrams.
From ZX-diagrams to quantum circuits with post-selection: deriving the translation from Picturing Quantum Software [section 3.4.1].
Application: proof of quantum teleportation protocol.

Support

Lecture Notes / Exercises
Projects for Assignments
Bibliography
Complementary Bibliography
Research blogs
Links

Pragmatics

Lecturers
Assessment
Contacts