diff --git a/index.xml b/index.xml index 6776cf8..5d42255 100644 --- a/index.xml +++ b/index.xml @@ -72,7 +72,7 @@ <tr> <td><a href="#nov-8">Nov 8</a></td> <td>Bhakti Shah</td> -<td><em>TBD</em></td> +<td>Proof Visualization for Graphical Structures</td> </tr> <tr> @@ -165,11 +165,11 @@ <p><strong>Speaker:</strong> Bhakti Shah</p> -<p><strong>Title:</strong> <em>TBD</em></p> +<p><strong>Title:</strong> Proof Visualization for Graphical Structures</p> -<p><strong>Abstract:</strong> <em>TBD</em></p> +<p><strong>Abstract:</strong> Reasoning about graphical languages in a proof assistant can be hard. Canonical diagrammatic representations are optimized for readability, and may abstract away details irrelevant to a pen-and-paper proof, but these details are often important to a proof assistant. We develop a methodology and library for working with graphical languages associated with classes of categories, and equip it with an automated visualizer integrated with the Coq proof assistant, enabling diagrammatic reasoning. We instantiate this with the ZX-calculus, a language for quantum computation, as an example of specialized diagrammatic reasoning.</p> -<p><strong>Bio:</strong> <em>TBD</em></p> +<p><strong>Bio:</strong> Bhakti Shah is a PhD student at the University of St. Andrews, advised by Edwin Brady, working on the interoperability of proof systems. She was previously at the University of Chicago, advised by Robert Rand, working on reasoning about diagrammatic languages in proof assistants. Her research interests broadly span the usability of interactive proof assistants.</p> <h2 id="nov-15">Nov 15</h2> diff --git a/lsd-seminar/2024fa/index.html b/lsd-seminar/2024fa/index.html index 5328edc..33572b6 100644 --- a/lsd-seminar/2024fa/index.html +++ b/lsd-seminar/2024fa/index.html @@ -253,7 +253,7 @@
Speaker: Bhakti Shah
-Title: TBD
+Title: Proof Visualization for Graphical Structures
-Abstract: TBD
+Abstract: Reasoning about graphical languages in a proof assistant can be hard. Canonical diagrammatic representations are optimized for readability, and may abstract away details irrelevant to a pen-and-paper proof, but these details are often important to a proof assistant. We develop a methodology and library for working with graphical languages associated with classes of categories, and equip it with an automated visualizer integrated with the Coq proof assistant, enabling diagrammatic reasoning. We instantiate this with the ZX-calculus, a language for quantum computation, as an example of specialized diagrammatic reasoning.
-Bio: TBD
+Bio: Bhakti Shah is a PhD student at the University of St. Andrews, advised by Edwin Brady, working on the interoperability of proof systems. She was previously at the University of Chicago, advised by Robert Rand, working on reasoning about diagrammatic languages in proof assistants. Her research interests broadly span the usability of interactive proof assistants.