IQPS: Introduction to Quantum Programming and Semantics
Welcome to Introduction to Quantum Programming and Semantics
Learning Outcomes
On successful completion of this course, you should be able to:
- identify features of current quantum programming platforms
- model quantum protocols categorically and prove their correctness graphically
- apply and prove basic results about monoidal categories
- fluently manipulate the graphical calculus for compact categories
- differentiate between categories modelling classical and quantum informatics
Course Outline
The course has two parallel tracks: a practical one, and a theoretical one. The practical track surveys different quantum programming platforms. These include OpenQAsm, Qiskit, Q#, Quipper, Quantomatic, and PyZX. We discuss their basic structure, strengths, and weaknesses. Via labs and live coding in lectures, students get hands-on experience of implementing small quantum programs. The emphasis is on the primitive programming constructs and structure of each language, not on large-scale quantum software development.
Simultaneously, the theoretical track analyses the features of each language in denotational semantics, focusing on monoidal categories. Via lectures and self-study reading, the course teaches students the basics of dual objects in monoidal categories. Specific attention is paid to the graphical calculus, which makes the topic visually apparent. Via exercise sheets, and their review incorporated into the contact hours, the student learns to graphically manipulate algebraic objects such as monoids and Frobenius structures. They will understand that this still allows perfectly rigorous proofs of correctness, and be able to see the information flow of a protocol that is often hidden behind superfluous details.
Throughout the course, the practical and theoretical material is linked. We will study notions typically thought to belong to quantum theory, such as entanglement, no-cloning, teleportation, and complementarity. It will turn out some of these notions also make perfect sense in other settings. For example, the very same categorical description of quantum teleportation also describes classical encryption with a one-time pad. We identify characteristics of classical and quantum information, aiming to equip students to choose the right tools and techniques for future problems they may encounter.