Overview

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.

Deadlines and Structure

All in-person meetings will take place in the seminar room for our chair. Route description.

Date Event
10.04, 14:00 Kick-off meeting
TBD Paper submission
TBD Presentation slides submission
TBD Seminar talks

Topics

Hoare Logic:

  1. Applied Hoare Logic: https://dl.acm.org/doi/pdf/10.1145/3314221.3314584 This paper introduces Hoare Logic with projective predicates and also consider robustness, that means including approximate satisfaction of predicates. Rather for Bachelor than for Master students
  2. Quantum Relational Hoare Logic: https://dl.acm.org/doi/pdf/10.1145/3290346 The paper introduces a logic for comparing two quantum programs (e.g., showing they do the same). Such logics are used for example in formal cryptography proofs.
  3. Quantum Hoare Logic with Ghost Variables: https://arxiv.org/pdf/1902.00325 The paper introduces a Hoare logic where one can use “ghost variables”, which are variables not occurring in the program, to be able to express additional properties such as non-entanglement, classicality and uniform distribution.
  4. Floyd Hoare Logic: https://dl.acm.org/doi/pdf/10.1145/2049706.2049708, Quantum Weakest Preconditions: https://arxiv.org/abs/quant-ph/0501157 Both of the mentioned papers consider Hoare logic but use hermitian operators instead of projective predicates. That means a predicate is not either satisfied or not but instead can be satisfied to a certain amount, e.g. to 40%.
  5. Expected Runtimes: https://arxiv.org/pdf/1911.12557 This paper also uses Hermitian predicates and is based on the same calculus as (4), but generalizes it to calculate the expected runtime of a program.

Other Logics:

  1. Incorrectness Logic: https://dl.acm.org/doi/pdf/10.1145/3527316 In comparison to Hoare logic (with the goal of verifying correctness), the goal of incorrectness logic is to find bugs.
  2. Separation Logic: https://arxiv.org/pdf/2102.00329 This paper considers a quantum interpretation of separation logic. Generally, for satisfaction in separation logic, a state/program is split up to satisfy parts of the predicate. Here the separation-part refers to whether a state can be split into two separate states (depends on entanglement) that satisfy the subpredicates.
  3. Quantum LTL: https://arxiv.org/pdf/1908.00158 In comparison to the other papers, this one is a temporal logic, a quantum extension of LTL (maybe known from e.g. the Model Checking lecture). The atomic sub formulas are projections. It also expresses Hoare triplets in terms of temporal logic formulas and studies decidability.