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, (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 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 Curry-Howard-Lambek correspondence.
  • Introduction to intuitionistic and linear logica.
  • Introduction to the lambda-calculus and its linear variant.
  • The Curry-Howard-Lambek correspondence for classical computation.
  • The Curry-Howard-Lambek 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 (2019-20)

  T Lectures

  • Sep 9 (9-11h): Introduction to the course: objectives, learning outcomes, organisation.

    Categories: definition and worked examples.

  • Sep 16 (11-13h): Functors. Definition and worked examples.

  • Sep 23 (9-11h): Universal properties. Intuition, characterization, examples. Final, initial and zero objects. Product and coproduct.
  • Oct 3 (9-11h) --- re-scheduled from 30 Set: Products and coproducts in different categories. Derivation of main laws. The cases of functions (Set), realtions and Hilbert spaces.
  • Oct 14 (9-11h): Natural transformations. Parametricty and uniforme transformation.
  • Oct 18 (9-11h) --- re-scheduled from 7 Oct: Representable functors. The lemma of Yoneda. Motivation and applications.
  • Oct 21 (9-11h) The logical side of the Curry-Howard-Lambek correspondence. Classical and intuitionistic logic, and corresponding proof theory (natural deduction and sequent calculus).
  • Oct 28 (9-11h) Semantics of classical and intuitionistic logic (Boolean algebras and Heyting algebras). The computational side of the Curry-Howard-Lambek correspondence. Introduction to the untyped lambda calculus.
  • Nov 4 (9-11h) Simply-typed lambda calculus and the Curry-Howard correspondence.
  • Nov 5 (10.30-12.30h) Quantum lambda calculus I (invited lecture by Benoit Valiron).
  • Nov 11 (9-11h) The classical Curry-Howard-Lambek correspondence - conclusion. Notion of adjunction; example: products and exponentials.
  • Nov 25 (9-11h) Monads. Programming with monads. (Lecture by Renato Neves, INESC TEC)
  • Dez 02 (9-11h) Introduction to dynamic logic. Extensions to quantum computation. (Lecture by Alexandre Madeira, UAveiro)
  • Dez 09 (9-11h) Quantum lambda calculus: syntax, operational semantics, typing system.

  P Lectures

  • Sep 9 (11-13h): Familiar and less familiar examples of categories. Exercises on defining / checking the strucutre of a category.
  • Sep 16 (14-16h) Exercises on rephrasing well-known, pointwise results in the language of categories: monos, epis and isos. Examples of functors.
  • Sep 23 (11-13h): 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 (11-13h) --- re-scheduled from 30 Set: Exercises on products and coproducts. Discussion of universal constructions.
  • Oct 14 (11h-13h): Natural transformations --- worked examples
  • Oct 18 (11-13h) --- re-scheduled from 7 Oct: Exercises on representable functors. Proof of the lemma of Yoneda.
  • Oct 21 (11h-13h): Exercises on intuitionistic propositional logic.
  • Oct 28 (11-13h): Exercises on the untyped lambda calculus
  • Nov 4 (9-11h) Exercises on the simply-typed lambda calculus and the Curry-Howard correspondence.
  • Nov 5 (14.30-16.30h) Quantum lambda calculus II (invited lecture by Benoit Valiron).
  • Nov 11 (11-13h) Exercises on the classical Curry-Howard-Lambek correspondence.
  • Nov 25 (11-13h) Exercises with monads. (Lecture by Renato Neves, INESC TEC)
  • Dez 09 (11-13h) Exercises on quantum lambda calculus: syntax, operational semantics, typing system.

  Support

  Lecture Notes / Exercises

  • Lecture 1: Categories
  • Lecture 2: Functors
  • Lecture 3: Universal properties
  • Lecture 4: Naturality
  • Lecture 5: Intuitionistic logic
  • Lecture 6: Untyped lambda calculus
  • Lecture 7: Simply-typed lambda calculus
  • Special Lecture: Quantum lambda calculus (Benoit Valiron)
  • Lecture 8: The classical Curry-Howard-Lambek correspondence
  • Lecture 9: Adjunctions
  • Lecture 10: Monads
  • Lecture 11: Quantum lambda calculus

  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.

  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. North-Holland, Elsevier, 2011.
  • ... other references will be suggested according to the lecturing scheduling.

  Links

  • Quantum Software Engineering Group no INL
  • Arca website no INESC TEC

  Pragmatics

  Lecturers

  • Luís Soares Barbosa
  • Renato Neves

  Assessment

  • Collection of written, individual, non presential assessments.

  Contacts

  • Appointments: Monday 16-18
  • Email: lsb arroba di ponto uminho ponto pt
  • Last update: 2019.11.03