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, (resource-sensitive) logic, and category theory, given by the Curry-Howard-Lambek correspondence, which identifies propositions with types and proofs with programs, and formalizes program semantics as a (monoidal) category;
• the specification of quantum algoritms and protocols in the (diagramatic) language of monoidal categories.

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

Syllabus

• Module 1: The Curry-Howard-Lambek correspondence for classical and quantum computation.
  • The Curry-Howard-Lambek isomorphism for intuitionistic logic.
  • The Curry-Howard-Lambek isomorphism for linear logic.
  • The Curry-Howard-Lambek isomorphism for quantum logic.
• Module 2: Specifying and reasoning about quantum programs in monoidal categories
  • Monoidal categories and string diagrams.
  • Computational interpretation of quantum mechanics. Associated categorical structures: monoidal (composition), compact closed (entanglement), adjunctions (internal product), biproduts (non deterministic branching).
  • Quantum processes.
  • The ZX-calculus.

Summaries (2023-24)

T Lectures

Feb 06 (11:00 - 13:00)	Introduction to the course: objectives, learning outcomes, organisation. The Curry-Howard-Lambek isomorphism for intuitionistic logic.
Feb 13 (11:00 - 13:00)	...
Apr 16 (11:00 - 13:00)	Diagrams and categories. Diagramatic languages for processes. Circuits [lecture notes]. String diagrams: definitions, examples, constructions [lecture notes].
Apr 24 (16:00 - 18:00)	The process theory of linear maps. Matricial representation. Completeness for string diagrams. [lecture notes] .(Room DI 1.20)
Apr 30 (11:00 - 11:00)	The process theory of pure quantum maps. Doubling to retrieve probabilities as scalars and get rid of global phases. [lecture notes] .

TP Lectures

Feb 06 (09:00 - 11:00)	Practice on the Curry-Howard-Lambek isomorphism for intuitionistic logic.
Feb 13 (09:00 - 11:00)	...
Apr 16 (09:00 - 11:00)	Exercises on circuits and string diagrams.
Apr 23 (09:00 - 11:00)	The ZX calculus [Wetering, 2020]
Apr 30 (09:00 - 11:00)	Exercises with linear maps

Support

Bibliography

• A. Pitts. Categorical logic. in Handbook of Logic in Computer Science (IV), Oxford University Press. (pdf)
• 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. (pdf)
• P. Selinger Lecture Notes on the Lambda Calculus . 2013. (link)
• B. Coecke and A. Kissinger. Picturing Quantum Processes: A First Course in Quantum Theory and Diagrammatic Reasoning . Cambridge University Press, 2017.

Complementary Bibliography

• A. S. Troelstra and H. Schwichtenberg. Basic Proof Theory. Cambridge University Press, 2012.
• C. Heunen and J. Vicary. Categories for Quantum Theory. Oxford Graduate Texts in Mathematics, 2019.
• 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 Lambda-Calculus 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. North-Holland, Elsevier, 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. (pdf)
• ... other references will be suggested according to the lecturing scheduling.

Research blogs

• nLab -- A wiki-lab 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 n-Category Café -- A group blog on math, physics and philosophy.

Links

• The ZX-calculus webpage
• The Quantum and Linear-Optical Computation Group at INL
• Arca website at INESC TEC

Pragmatics

Lecturers

• Luís Soares Barbosa
• Norihiro Yamada

Assessment

• (40%) Individual resolution of 6 take-home exercises along the semester (3 per each module)
  • Module 1: Exercise 1: due ...
  • Module 1: Exercise 2: due ...
  • Module 1: Exercise 3: due ...
  • Module 2: Exercise 1: due ...
  • Module 2: Exercise 2: due ...
  • Module 2: Exercise 3: due ...

• (60%) Written essay (1 per each module)
  • Module 1: Written essay: due 22 March
  • Module 2: Written essay: due 7 June

Contacts

• Lectures: T - Tuesday, 11-13 (Building 2, 1.09)| TP Tuesday 09-11(Building 2, 2.04)
• Appointments (Luís): Wed, 18:00-20:00 (please send an email the day before)
• Email: lsb arroba di ponto uminho ponto pt
• Appointments (Nori): Wed, 15:30-17:30 (please send an email the day before)
• Email: norihiro1988 arroba gmail ponto com
• Last update: 2024.04.29