Objectives and learning outcomes
The development of quantum information and computation entaisl the need for formal tools to model, verify and reason rigorously about quantum systems. 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 the quantum paradigm;

fundations, methods and tools 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, matricess, and Hilbert spaces.
 The CurryHowardLambek correspondence.
 Introduction to intuitionistic and linear logica.
 Introduction to the lambdacalculus and its linear variant.
 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 (201920)
T Lectures
P Lectures

Sep 9 (1113h):
Familiar and less familiar examples of categories. Exercises on defining / checking the strucutre of a category.

Sep 16 (1416h)
Exercises on rephrasing wellknown, pointwise results in the language of categories: monos, epis and isos.
Examples of functors.

Sep 23 (1113h):
Exercises on functors: forgetful and free functors; covariant and contravariant hom functors. Properties of functors. Preservation and reflection of properties by functors. Examples.

Oct 3 (1113h)  rescheduled from 30 Set:
Exercises on products and coproducts. Discussion of universal constructions.

Oct 14 (11h13h):
Natural transformations  worked examples

Oct 18 (1113h)  rescheduled from 7 Oct:
Exercises on representable functors. Proof of the lemma of Yoneda.

Oct 21 (11h13h):
Exercises on intuitionistic propositional logic.

Oct 28 (1113h):
Exercises on the untyped lambda calculus

Nov 4 (911h)
Exercises on the simplytyped lambda calculus and the CurryHoward correspondence.

Nov 5 (14.3016.30h)
Quantum lambda calculus II (invited lecture by Benoit Valiron).

Nov 11 (1113h)
Exercises on the classical CurryHowardLambek correspondence.

Nov 25 (1113h)
Exercises with monads.
(Lecture by Renato Neves, INESC TEC)

Dez 09 (1113h)
Exercises on quantum lambda calculus: syntax, operational semantics, typing system.
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.
Complementary Bibliography

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

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.
Links
Pragmatics
Lecturers
Assessment
 Collection of written, individual, non presential assessments.
Contacts
 Appointments: Monday 1618
 Email: lsb arroba di ponto uminho ponto pt
 Last update: 2019.11.03