Overview
- Responsible professor: Dominique Unruh
- Supervisors: Christina Gehnen, Dominique Unruh
- Semester: Summer 2025
- Level: Bachelor / Master
About
When designing programs/algorithms for quantum computers, one would like to know for sure what they do / whether they are correct. Like in the case of classical programs, it is possible to reason about programs using “program logics”. Examples of such logics (that you might know of from earlier courses) are Hoare logics, weakest precondition transformers, type systems, etc.
In this seminar, each participant will be studying one such program logic from a scientific paper, and present the results to their peers in a talk and a seminar report.
Prerequisites
You should have taken an introductory course related to quantum computing or quantum algorithms. (E.g., Introduction to Quantum Computing) It is beneficial if you have already studied logics in the classical settings (e.g. Hoare logics) in some context.