[CS] Adrian Lehmann Candidacy Exam/Dec.4th

[via cs]

This is an announcement of Adrian Lehmann's Candidacy Exam.
===============================================
Candidate: Adrian Lehmann

Date: Wednesday, December 4th

Time: 3PM CST 

Location: JCL 298

Remote Location: https://uchicago.zoom.us/j/97560499711?pwd=twL9qoCwLCEglJjawfEe2IZFtxSSqI.1 

Title: Proof Engineering for Quantum Reasoning via E-Graphs

Abstract: In this candidacy, I propose an exploration of quantum formal verification through the development of VyZX, a formalization of the ZX-calculus. VyZX uses the categorical structure of the ZX-calculus to reason about ZX diagrams, providing a framework to establish completeness, encode common rules, and reason about applications like peephole optimization. However, working within a symmetric monoidal category based representation introduces challenges, as the same ZX-diagram can have many equivalent representations in VyZX. This results in significant manual proof effort, as there is no single ``best'' normal form, which is both tedious and difficult to fully automate.

To address this, I propose a proof automation system that builds on E-Graphs, a data structure for managing equivalence classes. This system will streamline reasoning about equivalence of VyZX diagrams. While the primary focus is solving between different representations of semantically equivalent diagrams, I propose to explore the practical limits of solving more complex equalities. Finally, I propose extending these ideas to general dependently-typed inductive datatypes with equivalence relations, a common pattern in formal verification.

Advisors: John Reppy

Committee: Robert Rand, John Reppy, Jens Palsberg