<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=us-ascii">
</head>
<body style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class="">
This is an announcement of Youngchan Cho's MS Presentation<br class="">
===============================================<br class="">
Candidate: Youngchan Cho<br class="">
<br class="">
Date: Friday, May 31, 2024<br class="">
<br class="">
Time: 10:30 am CT<br class="">
<br class="">
Location: JCL 390<br class="">
<br class="">
Title: Formalizing a Lightweight Logic for Quantum Programs<br class="">
<br class="">
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.<br class="">
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.<br class="">
<br class="">
Advisors: Robert Rand<br class="">
<br class="">
Committee Members: Robert Rand, Fred Chong, and Stuart Kurtz<br class="">
<div class="">
<div dir="auto" style="caret-color: rgb(0, 0, 0); color: rgb(0, 0, 0); letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px; text-decoration: none; word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class="">
<div dir="auto" style="caret-color: rgb(0, 0, 0); color: rgb(0, 0, 0); letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px; text-decoration: none; word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class="">
<div dir="auto" style="caret-color: rgb(0, 0, 0); color: rgb(0, 0, 0); letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px; text-decoration: none; word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class="">
<div dir="auto" style="caret-color: rgb(0, 0, 0); color: rgb(0, 0, 0); letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px; text-decoration: none; word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class="">
<div dir="auto" style="caret-color: rgb(0, 0, 0); color: rgb(0, 0, 0); letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px; text-decoration: none; word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class="">
<div dir="auto" style="caret-color: rgb(0, 0, 0); color: rgb(0, 0, 0); letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px; text-decoration: none; word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class="">
<br class="Apple-interchange-newline">
</div>
<br class="Apple-interchange-newline">
</div>
<br class="Apple-interchange-newline">
</div>
<br class="Apple-interchange-newline">
</div>
<br class="Apple-interchange-newline">
</div>
<br class="Apple-interchange-newline">
</div>
<br class="Apple-interchange-newline">
<br class="Apple-interchange-newline">
</div>
<br class="">
</body>
</html>