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 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.

Assessment: List of Research Exercises

All information available HERE

Syllabus

• Categories for quantum computing
  • Categories, funtors, and natural transformations.
  • Universal properties and adjunctions.
  • Monoidal categories; Aplications: (categories of) relations, matrices, and Hilbert spaces.
• 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.
• The Curry-Howard-Lambek correspondence.
  • Introduction to intuitionistic and linear logic.
  • Introduction to the simply-typed lambda-calculus.
  • Quantum lambda-calculus.
  • The Curry-Howard-Lambek correspondence for classical computation.
  • The Curry-Howard-Lambek correspondence for quantum computation.

  Summaries (2020-21)

  T Lectures

  • Oct 6 (14-16h): Introduction to the course: objectives, learning outcomes, organisation.

    Categories: definition and worked examples.

    Live session 1: Join on zoom here!

  • Oct 13 (14-16h):

    Functors: definition and worked examples.

    Live session 2: Join on zoom here!

  • Oct 23 (14-16h):

    Introduction to universal properties. Initial and final objects. Products and coproducts: definions, examples, properties.

    Live session 3: Join on zoom here!

  • Oct 30 (14-16h):

    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!

  • Nov 06 (14-16h):

    Processes and diagrams. Monoidal categories and representation of process theories. Introduction to diagramatic reasoning.

    Live session 5: Join on zoom here!

  • Nov 13 (14-16h):

    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!

  P Lectures

  • Oct, 12 (09-11h): Familiar and less familiar examples of categories. Exercises on defining / checking the strucutre of a category. Exercises on rephrasing well-known, pointwise results in the language of categories: Isomorphisms, monomorphisms and epimorphisms.
  • Oct, 19 (09-11h): Exercises on functors. Full and faithful functors. The categories CAT and Cat. Isomorphisms between categories.
  • Oct, 26 (09-11h): Exercises on universal properties. Product and co-product: examples and properties.
  • Nov, 06 (16-18h): Exercises on natural transformations.

    Live session: Join on zoom here!

  • Nov, 9 (09-11h): Exercises on circuits and monoidal categories (symmetric, strict and non strict).
  • Nov, 16 (09-11h): Exercises on string diagrams.
  • Nov, 23 (09-11h): Exercises on string diagrams. An example of equivalence of categories.
  • Dec, 3 (09-11h): Exercises on the theory of linear maps.
  • Dec, 15 (09-11h): Exercises on the theory of quantum processes. The teleportation protocol (handwritten note) .
  • Jan, 4 (09-11h): Exercises on lambda calculus and intuitionistic logic.
  • Jan, 11 (09-11h): Exercises on typed lambda calculus and the CHL correspondence for classical computation.

  Support

  Lecture Notes / Exercises

  • Lecture 1: Categories
  • Lecture 2: Functors
  • Lecture 3: Universal properties
  • Lecture 4: Naturality
  • Lecture 5: Diagrams, processes and monoidal categories
  • Lecture 6: String diagrams and dagger categories - I
  • Lecture 7: String diagrams and dagger categories - II
  • Lecture 8: A process theory for linear maps
  • Lecture 9: A process theory for pure quantum maps
  • Lecture 10: The theory of quantum processes
  • Lecture 11: Untyped lambda calculus
  • Lecture 12: An introduction to intuitionistic logic
  • Lecture 13: Simply typed lambda calculus
  • Lecture 14: The Curry-Howard-Lambek correspondence for classical computation
  • Lecture 15: A quantum lambda calculus. The Curry-Howard-Lambek correspondence for quantum computation

  Reference papers

  • Introduction to Categories and Categorical Logic (S. Abramsky and N. Tzevelekos, 2011)
  • Physics, Topology, Logic and Computation: A Rosetta Stone (J. Baez and M. Stay, 2011)

  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 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.
  • ... 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 Quantum Software Engineering Group and Quantum and Linear-Optical Computation Group at INL
  • Arca website at INESC TEC

  Pragmatics

  Lecturer

  • Luís Soares Barbosa
  • Renato Neves

  Assessment

  • Individual paper recitation and written essay

    Presentation and discussion: Friday, Mar 5

  Contacts

  • Lectures: T - Tuesday, 14-16 | TP Monday 09-11
  • Appointments: Friday 16-18
  • Email: lsb arroba di ponto uminho ponto pt
  • Last update: 2021.01.17