[CS] Benjamin Caldwell Candidacy Exam/Sep 26, 2025

[via cs]

This is an announcement of Benjamin Caldwell's Candidacy Exam.
===============================================
Candidate: Benjamin Caldwell

Date: Friday, September 26, 2025

Time: 10 am CST

Location: JCL 205

Title: Verifying Diagrammatic Calculi

Abstract: Our development of VyZX, a verified library for the ZX-calculus, highlighted a critical and general challenge in proof assistants: the lack of a framework for formally implementing diverse diagrammatic calculi. Each new calculus requires a bespoke effort. This dissertation proposes to solve this problem by generalizing the lessons learned from VyZX. We will design and implement a flexible system in the Rocq proof assistant, by utilizing the theory of abstract tensor systems and the Rocq module system, that allows users to define their own diagrammatic languages. Building upon the block-structure representations developed for VyZX, the proposed framework will enable users to specify custom "generators" and visualize the resulting diagrams. The goal is to drastically reduce the effort required to formally verify graphical languages. We will validate this framework by applying it to key targets in quantum information, such as the ZH-calculus, and exploring its power on more complex structures like the tensor networks used in quantum simulation and machine learning. Ultimately, this research aims to provide a trusted tool for researchers to rapidly prototype, verify, and discover new theorems in a wide range of graphical calculi.


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