Update 2024fa.md

lsd-ucsc · Nov 7, 2024 · 765fc8f · 765fc8f
1 parent fe24cf5
commit 765fc8f
Showing 1 changed file with 4 additions and 4 deletions.
diff --git a/content/lsd-seminar/2024fa.md b/content/lsd-seminar/2024fa.md
@@ -24,7 +24,7 @@ Talks will be advertised on the [ucsc-lsd-seminar-announce](https://groups.googl
 | [Oct 18](#oct-18)     | Bastian Köpcke                                                        | Descend: A Safe Imperative GPU Programming Language |
 | [Oct 25](#oct-25)     | Haofan Zheng                                                          | Decentagram: Highly-Available Decentralized Publish/Subscribe Systems |
 | [Nov 1](#nov-1)       | Justin Lubin                                                          | Programming By Navigation |
-| [Nov 8](#nov-8)       | Bhakti Shah                                                           | _TBD_ |
+| [Nov 8](#nov-8)       | Bhakti Shah                                                           | Proof Visualization for Graphical Structures |
 | [Nov 15](#nov-15)     | Federico Mora                                                         | _TBD_ |
 | [Nov 22](#nov-22)     | Haining Tong                                                          | _TBD_ |
 | [Dec 6](#dec-6)       | Yanan Guo                                                             | _TBD_ |
@@ -99,11 +99,11 @@ More broadly, I’ll talk about our deep, ongoing collaboration with experimenta
 
 **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. 
 
 ## Nov 15