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 the connection between (quantum) computation, (resource-sensitive) logic, and category theory, given by the Curry-Howard-Lambek correspondence, which identifies propositions with types and proofs with programs, and formalizes the model space as a (monoidal) category. Thus, in the end, students will be able to apply to the development of quantum programs a solid and operative knowledge in
Categories: definition and worked examples.
Live session 1: Join on zoom here!
Functors: definition and worked examples.
Live session 2: Join on zoom here!
Introduction to universal properties. Initial and final objects. Products and coproducts: definions, examples, properties.
Live session 3: Join on zoom here!
Naturality, the last corner of the categorical imperative (Functoriality, Universality, Naturality). Examples of natural transformations. Composition. Equivalence of categories.
Live session 4: Join on zoom here!
Processes and diagrams. Monoidal categories and representation of process theories. Introduction to diagramatic reasoning.
Live session 5: Join on zoom here!
String diagrams. Non-separability. Representing transpose, adjoint, trace, conjugate, and inner product.
Live session 6: Join on zoom here!Nov 20 (14-16h):
Unitary processes, positive processes and projectors in string diagrams. Expressing quatum phenomena in theories interpreted over string diagrams. Dagger compact-closed categories.
Live session 7: Join on zoom here!Nov 27 (14-16h):
Basis and sums in string diagrams --- towards a process theory of linear maps. From processes to matrices and back.
Live session 8: Join on zoom here!Dec 7 (09-11h):
The process theory of linear maps: conclusion. From linear maps to (pure) quantum maps. Process doubling.
Live session 9: Join on zoom here!Dec 11 (13-15h):
Quantum processes. Discarding. Causality. Non-determinism. The theory of quantum processes.
Live session 10: Join on zoom here!Dec 18 (14-16h):
Introduction to the Curry-Howard-Lambek correspondence. Untyped lambda-calculus. A glimpse over intuitionistic logic.
Live session 11: Join on zoom here!Jan 8 (14-16h):
Simply-types yped lambda-calculus. The Curry-Howard-Lambek correspondence for classical computation.
Live session 12: Join on zoom here!Jan 18 (09-11h):
Quantum lambda-calculus. A brief mention to linear logic and the Curry-Howard-Lambek correspondence for quantum computation.
Live session 13: Join on zoom here!
Live session: Join on zoom here!
Presentation and discussion: Friday, Mar 5