Quantum Logic (2020-21)

MIEFis - MSc in Physics Engineering

Dep. Informática, Universidade do Minho

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