regenerate after: Update 2024fa.md

lsd-ucsc · Nov 7, 2024 · eb82f87 · eb82f87
1 parent 736cffa
commit eb82f87
Show file tree

Hide file tree

Showing 3 changed files with 8 additions and 9 deletions.
diff --git a/index.xml b/index.xml
@@ -72,7 +72,7 @@
 &lt;tr&gt;
 &lt;td&gt;&lt;a href=&#34;#nov-8&#34;&gt;Nov 8&lt;/a&gt;&lt;/td&gt;
 &lt;td&gt;Bhakti Shah&lt;/td&gt;
-&lt;td&gt;&lt;em&gt;TBD&lt;/em&gt;&lt;/td&gt;
+&lt;td&gt;Proof Visualization for Graphical Structures&lt;/td&gt;
 &lt;/tr&gt;
 
 &lt;tr&gt;
@@ -165,11 +165,11 @@
 
 &lt;p&gt;&lt;strong&gt;Speaker:&lt;/strong&gt; Bhakti Shah&lt;/p&gt;
 
-&lt;p&gt;&lt;strong&gt;Title:&lt;/strong&gt; &lt;em&gt;TBD&lt;/em&gt;&lt;/p&gt;
+&lt;p&gt;&lt;strong&gt;Title:&lt;/strong&gt; Proof Visualization for Graphical Structures&lt;/p&gt;
 
-&lt;p&gt;&lt;strong&gt;Abstract:&lt;/strong&gt; &lt;em&gt;TBD&lt;/em&gt;&lt;/p&gt;
+&lt;p&gt;&lt;strong&gt;Abstract:&lt;/strong&gt; 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.&lt;/p&gt;
 
-&lt;p&gt;&lt;strong&gt;Bio:&lt;/strong&gt; &lt;em&gt;TBD&lt;/em&gt;&lt;/p&gt;
+&lt;p&gt;&lt;strong&gt;Bio:&lt;/strong&gt; 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.&lt;/p&gt;
 
 &lt;h2 id=&#34;nov-15&#34;&gt;Nov 15&lt;/h2&gt;
 

diff --git a/lsd-seminar/2024fa/index.html b/lsd-seminar/2024fa/index.html
@@ -253,7 +253,7 @@ <h1 itemprop="name">Languages, Systems, and Data Seminar (Fall 2024)</h1>
 <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>
@@ -346,11 +346,11 @@ <h2 id="nov-8">Nov 8</h2>
 
 <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/themes/academic b/themes/academic