regenerate after: Add Elaine's talk info

lsd-ucsc · Oct 20, 2023 · 24723f6 · 24723f6
1 parent 2ad100e
commit 24723f6
Show file tree

Hide file tree

Showing 3 changed files with 13 additions and 8 deletions.
diff --git a/index.xml b/index.xml
@@ -66,7 +66,7 @@
 &lt;tr&gt;
 &lt;td&gt;&lt;a href=&#34;#oct-27&#34;&gt;Oct. 27&lt;/a&gt;&lt;/td&gt;
 &lt;td&gt;Elaine Li&lt;/td&gt;
-&lt;td&gt;TBD&lt;/td&gt;
+&lt;td&gt;Multiparty Session Type Projection and Subtyping with Automata&lt;/td&gt;
 &lt;/tr&gt;
 
 &lt;tr&gt;
@@ -202,11 +202,13 @@ publication list, blog, and other information at &lt;a href=&#34;https://harriso
 
 &lt;p&gt;&lt;strong&gt;Speaker:&lt;/strong&gt; Elaine Li&lt;/p&gt;
 
-&lt;p&gt;&lt;strong&gt;Title:&lt;/strong&gt; TBD&lt;/p&gt;
+&lt;p&gt;&lt;strong&gt;Title:&lt;/strong&gt; Multiparty Session Type Projection and Subtyping with Automata&lt;/p&gt;
 
-&lt;p&gt;&lt;strong&gt;Abstract:&lt;/strong&gt; TBD&lt;/p&gt;
+&lt;p&gt;&lt;strong&gt;Abstract:&lt;/strong&gt; Multiparty session types (MSTs) are a type-based approach to verifying communication protocols. Central to MSTs is a projection operator: a partial function that maps protocols represented as global types to correct-by-construction implementations for each participant, represented as a communicating state machine (CSM). Existing projection operators are syntactic in nature, and trade efficiency for completeness. In the first part of the talk, I will present the first projection operator that is sound and complete. I will highlight the automata-theoretic nature of our projection operator, which separates synthesis from checking implementability. For synthesis, we use a simple subset construction; for checking implementability, we present succinct conditions that summarize insights into the property of implementability. We use these conditions to show that MST implementability is PSPACE-complete.&lt;/p&gt;
 
-&lt;p&gt;&lt;strong&gt;Bio:&lt;/strong&gt; TBD&lt;/p&gt;
+&lt;p&gt;While our projection operator always computes a candidate implementation if one exists, it may not always be the best candidate. In the second part of the talk, I motivate the subtyping problem for MSTs through a series of examples. I then demonstrate how we can use our conditions from before to obtain decidability results for MST subtyping with unrestricted CSMs as implementation model.&lt;/p&gt;
+
+&lt;p&gt;&lt;strong&gt;Bio:&lt;/strong&gt; Elaine Li is a fourth year PhD student at New York University, working with Thomas Wies. She is interested in both the theory and practice of protocol verification, and her PhD research focuses on the theory of multiparty session types.&lt;/p&gt;
 
 &lt;h1 id=&#34;nov-3&#34;&gt;Nov. 3&lt;/h1&gt;
 

diff --git a/lsd-seminar/2023fa/index.html b/lsd-seminar/2023fa/index.html
@@ -247,7 +247,7 @@ <h1 itemprop="name">Languages, Systems, and Data Seminar (Fall 2023)</h1>
 <tr>
 <td><a href="#oct-27">Oct. 27</a></td>
 <td>Elaine Li</td>
-<td>TBD</td>
+<td>Multiparty Session Type Projection and Subtyping with Automata</td>
 </tr>
 
 <tr>
@@ -383,11 +383,13 @@ <h1 id="oct-27">Oct. 27</h1>
 
 <p><strong>Speaker:</strong> Elaine Li</p>
 
-<p><strong>Title:</strong> TBD</p>
+<p><strong>Title:</strong> Multiparty Session Type Projection and Subtyping with Automata</p>
 
-<p><strong>Abstract:</strong> TBD</p>
+<p><strong>Abstract:</strong> Multiparty session types (MSTs) are a type-based approach to verifying communication protocols. Central to MSTs is a projection operator: a partial function that maps protocols represented as global types to correct-by-construction implementations for each participant, represented as a communicating state machine (CSM). Existing projection operators are syntactic in nature, and trade efficiency for completeness. In the first part of the talk, I will present the first projection operator that is sound and complete. I will highlight the automata-theoretic nature of our projection operator, which separates synthesis from checking implementability. For synthesis, we use a simple subset construction; for checking implementability, we present succinct conditions that summarize insights into the property of implementability. We use these conditions to show that MST implementability is PSPACE-complete.</p>
 
-<p><strong>Bio:</strong> TBD</p>
+<p>While our projection operator always computes a candidate implementation if one exists, it may not always be the best candidate. In the second part of the talk, I motivate the subtyping problem for MSTs through a series of examples. I then demonstrate how we can use our conditions from before to obtain decidability results for MST subtyping with unrestricted CSMs as implementation model.</p>
+
+<p><strong>Bio:</strong> Elaine Li is a fourth year PhD student at New York University, working with Thomas Wies. She is interested in both the theory and practice of protocol verification, and her PhD research focuses on the theory of multiparty session types.</p>
 
 <h1 id="nov-3">Nov. 3</h1>
 

diff --git a/themes/academic b/themes/academic