From 24723f633a8ab2dff523c2f206990f4e8b5d1a1c Mon Sep 17 00:00:00 2001 From: lkuper Date: Fri, 20 Oct 2023 20:17:15 +0000 Subject: [PATCH] regenerate after: Add Elaine's talk info --- index.xml | 10 ++++++---- lsd-seminar/2023fa/index.html | 10 ++++++---- themes/academic | 1 + 3 files changed, 13 insertions(+), 8 deletions(-) create mode 160000 themes/academic diff --git a/index.xml b/index.xml index ef58f4f..4b737ee 100644 --- a/index.xml +++ b/index.xml @@ -66,7 +66,7 @@ <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> @@ -202,11 +202,13 @@ publication list, blog, and other information at <a href="https://harriso <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/lsd-seminar/2023fa/index.html b/lsd-seminar/2023fa/index.html index cf845a9..7ce9fc8 100644 --- a/lsd-seminar/2023fa/index.html +++ b/lsd-seminar/2023fa/index.html @@ -247,7 +247,7 @@

Languages, Systems, and Data Seminar (Fall 2023)

Oct. 27 Elaine Li -TBD +Multiparty Session Type Projection and Subtyping with Automata @@ -383,11 +383,13 @@

Oct. 27

Speaker: Elaine Li

-

Title: TBD

+

Title: Multiparty Session Type Projection and Subtyping with Automata

-

Abstract: TBD

+

Abstract: 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.

-

Bio: TBD

+

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.

+ +

Bio: 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.

Nov. 3

diff --git a/themes/academic b/themes/academic new file mode 160000 index 0000000..8d596ff --- /dev/null +++ b/themes/academic @@ -0,0 +1 @@ +Subproject commit 8d596ffed2d080010c561679cf4e9b4da1554781