[Colloquium] Youngchan Cho MS Presentation/May 31, 2024

[via Colloquium]

This is an announcement of Youngchan Cho's MS Presentation
===============================================
Candidate: Youngchan Cho

Date: Friday, May 31, 2024

Time: 10:30 am CT

Location: JCL 390

Title: Formalizing a Lightweight Logic for Quantum Programs

Abstract: This paper introduces a formalization of a Hoare-logic style system for quantum programs using Clifford+T gates. Specifically, it formalizes the existing "Hoare-Heisenberg logic" based on the Heisenberg representation of quantum computation. Under the Heisenberg representation, quantum operations act as a mapping between quantum operations. Following the Heisenberg representation, in Hoare-Heisenberg logic, quantum programs using Clifford+T gates act as a mapping between predicates which is an augmented n-qubit Pauli group. Equivalently, quantum programs using Clifford+T gates act as a mapping between the +1 eigenvectors of predicates. To formalize this equivalence, we expand the Coq library QuantumLib to include the definition of vector spaces and some lemmas about the dimensions of a vector space such as lemmas stating that dimensions are uniquely defined for every vector space, a set of vectors whose cardinality is larger than the dimension is linearly dependent, and given a set of vectors whose cardinality equals the dimension of the vector space, the set of vectors is linearly independent if and only if it spans the vector space.
To formalize Hoare-Heisenberg logic, this work makes changes to certain definitions so that the logic system guarantees atomic predicates of the logic (which are represented as matrices) to be trace-zero, unitary, and Hermitian. Three notable changes are: 1. In the inductive definition of predicates, we separate the implementation of tensored terms from additive terms. This allows a more incremental implementation of guarantees for trace-zero, unitary, and Hermitian predicates. 2. By introducing a notion of well-formedness, we implement a strict type checker to guarantee trace-zero, unitary, and Hermitian predicates. 3. The application of inference rules are more strict, only allowing well-formed predicates that are guaranteed to have trace-zero, unitary, and Hermitian predicates. Our goal is to finish implementing the other features of Hoare-Heisenberg logic such as separability and apply this logic system to other areas such as reasoning about quantum correcting codes.

Advisors: Robert Rand

Committee Members: Robert Rand, Fred Chong, and Stuart Kurtz