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 the connection between (quantum) computation, (resourcesensitive) logic, and category theory, given by the CurryHowardLambek 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

semantics and calculi for quantum programs;

logics for the specification and verification of quantum programs.
Syllabus
 Categories for quantum computing
 Categories, funtors, and natural transformations.
 Universal properties and adjunctions.
 Monoidal categories; Aplications: (categories of) relations, matrices, and Hilbert spaces.
 The CurryHowardLambek correspondence.
 Introduction to intuitionistic and linear logica.
 Introduction to the simplytyped lambdacalculus.
 Quantum lambdacalculus.
 The CurryHowardLambek correspondence for classical computation.
 The CurryHowardLambek correspondence for quantum computation.
 Diagramatic reasoning in monoidal categories
 Diagramatic representations of monoidal categories. String diagrams.
 Computational interpretation of quantum mechanics; associated categorical structures: monoidal (composition), compact closed (entanglement), adjunctions (internal product), biproduts (non deterministic branching).
 Quantum processes.
Summaries (202021)
T Lectures

Oct 6 (1416h):
Introduction to the course: objectives, learning outcomes, organisation.
Categories: definition and worked examples.
Live session 1: Join on zoom
here!
Oct 13 (1416h):
Functors: definition and worked examples.
Live session 2: Join on zoom
here!
Oct 23 (1416h):
Introduction to universal properties. Initial and final objects. Products and coproducts: definions, examples, properties.
Live session 3: Join on zoom
here!
P Lectures

Oct, 12 (0911h):
Familiar and less familiar examples of categories. Exercises on defining / checking the strucutre of a category. Exercises on rephrasing wellknown, pointwise results in the language of categories: Isomorphisms, monomorphisms and epimorphisms.

Oct, 19 (0911h):
Exercises on functors. Full and faithful functors. The categories CAT and Cat. Isomorphisms between categories.
Support
Lecture Notes / Exercises
Reference papers
Bibliography

S. Abramsky and N. Tzevelekos. Introduction to categories and categorical logic. In B. Coecke,
editor, New Structures for Physics, pages 3–94. Springer Lecture Notes on Physics
(813), 2011.

J. Baez and M. Stay. Physics, topology, logic and computation: A Rosetta stone. In B. Coecke,
editor, New Structures for Physics, pages 95–172. Springer Lecture Notes on Physics
(813), 2011.

B. Coecke and A. Kissinger. Picturing Quantum Processes: A First Course in Quantum
Theory and Diagrammatic Reasoning . Cambridge University Press, 2017.

C. Heunen and J. Vicary. Categories for Quantum Theory. Oxford Graduate Texts in Mathematics, 2019.
Complementary Bibliography

S. Awodey. Category Theory. Oxford Logic Guides. Oxford University Press, 2006.

Emily Riehl. Category Theory in Context. Aurora  Dover Modern Math Originals, 2019.

J. R. Hindley and J. P. Seldin LambdaCalculus and Combinators, an Introduction. Cambridge University Press, 2008.

S. Abramsky and B. Coecke. Categorical quantum mechanics. In Kurt Engesser, Dov Gabbay,
and Daniel Lehmann, editors, Handbook of Quantum Logic and Quantum Structures,
pages 261–324. NorthHolland, Elsevier, 2011.

... other references will be suggested according to the lecturing scheduling.
Research blogs
 nLab  A wikilab for collaborative work on Mathematics, Physics and Philosophy in so far as these subjects are usefully treated with tools and notions of category theory.
 Graphical Linear Algebra  Pawel Sobocinski's blog about rediscovering linear algebra in a compositional way, with string diagrams.
 The nCategory Café  A group blog on math, physics and philosophy.
Links
Pragmatics
Lecturer
Assessment
 Individual paper recitation and written essay.
Contacts
 Lectures: T  Tuesday, 1416  TP Monday 0911
 Appointments: Friday 1618
 Email: lsb arroba di ponto uminho ponto pt
 Last update: 2020.10.23