[logic-ml] 吉田展子先生講演(8/1 14:00~ @ 早稲田大学)

[Tachio Terauchi]

皆様、

先ほどお送りした講演のご案内ですが、曜日が間違っておりました。正しくは、

日時： 8月1日(火) 14:00 ～

となります。(上田先生ご指摘ありがとうございます。)

どうぞよろしくお願いいたします。

寺内

On Tue, Jul 11, 2023 at 1:12 PM Tachio Terauchi <terauchi at waseda.jp> wrote:

> 皆さま、
>
> 8月1日に早稲田大学にて吉田展子先生によるご講演があります。
> 詳細は下記の通りです。
> よろしければぜひご参加ください。
>
> -----
> 日時： 8月1日(水) 14:00 ～
>
> 場所： 早稲田大学 西早稲田キャンパス 63号館 5階506室
>
> 題目： Multiparty Session Types: Specification-Guided Parallel and
> Distributed Programming
>
> 講演者: Nobuko Yoshida (University of Oxford)
>
> 概要：
> I first give a gentle introduction of multiparty session types. Then I
> will talk about a joint work with Zak Cutner and Martin Vassor.
>
> Rust is a modern systems language focused on performance and reliability.
> Complementing Rust's promise to provide "fearless concurrency", developers
> frequently exploit asynchronous message passing. Unfortunately, sending and
> receiving messages in an arbitrary order to maximise
> computation-communication overlap (a popular optimisation in
> message-passing applications) opens up a Pandora's box of subtle
> concurrency bugs.
>
>  To guarantee deadlock-freedom by construction, we present Rumpsteak: a
> new Rust framework based on multiparty session types. Previous session type
> implementations in Rust are either built upon synchronous and blocking
> communication and/or are limited to two-party interactions. Crucially, none
> support the arbitrary ordering of messages for efficiency.
>
>  Rumpsteak instead targets asynchronous async/await code. Its unique
> ability is allowing developers to arbitrarily order send/receive messages
> while preserving deadlock-freedom. For this, Rumpsteak incorporates two
> recent advanced session type theories: (1) k-multiparty compatibility
> (k-MC), which globally verifies the safety of a set of participants, and
> (2) asynchronous multiparty session subtyping, which locally verifies
> optimisations in the context of a single participant. Specifically, we
> propose a novel algorithm for asynchronous subtyping that is both sound and
> decidable.
>
>  We first talk about Rumsteak and show the new algorithm. We then talk
> about evaluations against other Rust implementations and asynchronous
> verification tools.
> ----
>
> 寺内
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.fos.kuis.kyoto-u.ac.jp/pipermail/logic-ml/attachments/20230711/ef36c093/attachment.htm>