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

[Tachio Terauchi]

皆様、

明日の講演のリマインダーをお送りいたします。

なお、明日は早稲田キャンパス<->西早稲田キャンパス間のシャトルバスは運休ですので、ご注意下さい。

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

寺内

2023年7月11日(火) 15:12 Tachio Terauchi <terauchi at waseda.jp>:

> 皆様、
>
> 先ほどお送りした講演のご案内ですが、曜日が間違っておりました。正しくは、
>
> 日時： 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/20230731/37566ed0/attachment.htm>