2 Search Results for "Kokke, Wen"

Document
DOI: 10.4230/LIPIcs.ECOOP.2022.4
Stay Safe Under Panic: Affine Rust Programming with Multiparty Session Types

Authors: Nicolas Lagaillardie, Rumyana Neykova, and Nobuko Yoshida

Published in: LIPIcs, Volume 222, 36th European Conference on Object-Oriented Programming (ECOOP 2022)

Abstract
Communicating systems comprise diverse software components across networks. To ensure their robustness, modern programming languages such as Rust provide both strongly typed channels, whose usage is guaranteed to be affine (at most once), and cancellation operations over binary channels. For coordinating components to correctly communicate and synchronise with each other, we use the structuring mechanism from multiparty session types, extending it with affine communication channels and implicit/explicit cancellation mechanisms. This new typing discipline, affine multiparty session types (AMPST), ensures cancellation termination of multiple, independently running components and guarantees that communication will not get stuck due to error or abrupt termination. Guided by AMPST, we implemented an automated generation tool (MultiCrusty) of Rust APIs associated with cancellation termination algorithms, by which the Rust compiler auto-detects unsafe programs. Our evaluation shows that MultiCrusty provides an efficient mechanism for communication, synchronisation and propagation of the notifications of cancellation for arbitrary processes. We have implemented several usecases, including popular application protocols (OAuth, SMTP), and protocols with exception handling patterns (circuit breaker, distributed logging).
Cite as

Nicolas Lagaillardie, Rumyana Neykova, and Nobuko Yoshida. Stay Safe Under Panic: Affine Rust Programming with Multiparty Session Types. In 36th European Conference on Object-Oriented Programming (ECOOP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 222, pp. 4:1-4:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{lagaillardie_et_al:LIPIcs.ECOOP.2022.4,
  author =	{Lagaillardie, Nicolas and Neykova, Rumyana and Yoshida, Nobuko},
  title =	{{Stay Safe Under Panic: Affine Rust Programming with Multiparty Session Types}},
  booktitle =	{36th European Conference on Object-Oriented Programming (ECOOP 2022)},
  pages =	{4:1--4:29},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-225-9},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{222},
  editor =	{Ali, Karim and Vitek, Jan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2022.4},
  URN =		{urn:nbn:de:0030-drops-162324},
  doi =		{10.4230/LIPIcs.ECOOP.2022.4},
  annote =	{Keywords: Rust language, affine multiparty session types, failures, cancellation}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2021.36
Separating Sessions Smoothly

Authors: Simon Fowler, Wen Kokke, Ornela Dardha, Sam Lindley, and J. Garrett Morris

Published in: LIPIcs, Volume 203, 32nd International Conference on Concurrency Theory (CONCUR 2021)

Abstract
This paper introduces Hypersequent GV (HGV), a modular and extensible core calculus for functional programming with session types that enjoys deadlock freedom, confluence, and strong normalisation. HGV exploits hyper-environments, which are collections of type environments, to ensure that structural congruence is type preserving. As a consequence we obtain a tight operational correspondence between HGV and HCP, a hypersequent-based process-calculus interpretation of classical linear logic. Our translations from HGV to HCP and vice-versa both preserve and reflect reduction. HGV scales smoothly to support Girard’s Mix rule, a crucial ingredient for channel forwarding and exceptions.
Cite as

Simon Fowler, Wen Kokke, Ornela Dardha, Sam Lindley, and J. Garrett Morris. Separating Sessions Smoothly. In 32nd International Conference on Concurrency Theory (CONCUR 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 203, pp. 36:1-36:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{fowler_et_al:LIPIcs.CONCUR.2021.36,
  author =	{Fowler, Simon and Kokke, Wen and Dardha, Ornela and Lindley, Sam and Morris, J. Garrett},
  title =	{{Separating Sessions Smoothly}},
  booktitle =	{32nd International Conference on Concurrency Theory (CONCUR 2021)},
  pages =	{36:1--36:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-203-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{203},
  editor =	{Haddad, Serge and Varacca, Daniele},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2021.36},
  URN =		{urn:nbn:de:0030-drops-144138},
  doi =		{10.4230/LIPIcs.CONCUR.2021.36},
  annote =	{Keywords: session types, hypersequents, linear lambda calculus}
}
  • Refine by Author
  • 1 Dardha, Ornela
  • 1 Fowler, Simon
  • 1 Kokke, Wen
  • 1 Lagaillardie, Nicolas
  • 1 Lindley, Sam
  • Show More...

  • Refine by Classification
  • 1 Software and its engineering → Concurrent programming languages
  • 1 Software and its engineering → Functional languages
  • 1 Software and its engineering → Software usability
  • 1 Theory of computation → Linear logic
  • 1 Theory of computation → Process calculi

  • Refine by Keyword
  • 1 Rust language
  • 1 affine multiparty session types
  • 1 cancellation
  • 1 failures
  • 1 hypersequents
  • Show More...

  • Refine by Type
  • 2 document

  • Refine by Publication Year
  • 1 2021
  • 1 2022

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact