DROPS

Document

Artifact

Ferrite: A Judgmental Embedding of Session Types in Rust (Artifact)

Authors: Ruo Fei Chen, Stephanie Balzer, and Bernardo Toninho

Published in: DARTS, Volume 8, Issue 2, Special Issue of the 36th European Conference on Object-Oriented Programming (ECOOP 2022)

Abstract

This artifact provides a VirtualBox image containing the snapshots of source code for Ferrite and Servo at the time the main paper was published.

Cite as

Ruo Fei Chen, Stephanie Balzer, and Bernardo Toninho. Ferrite: A Judgmental Embedding of Session Types in Rust (Artifact). In Special Issue of the 36th European Conference on Object-Oriented Programming (ECOOP 2022). Dagstuhl Artifacts Series (DARTS), Volume 8, Issue 2, pp. 14:1-14:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@Article{chen_et_al:DARTS.8.2.14,
  author =	{Chen, Ruo Fei and Balzer, Stephanie and Toninho, Bernardo},
  title =	{{Ferrite: A Judgmental Embedding of Session Types in Rust (Artifact)}},
  pages =	{14:1--14:2},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2022},
  volume =	{8},
  number =	{2},
  editor =	{Chen, Ruo Fei and Balzer, Stephanie and Toninho, Bernardo},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DARTS.8.2.14},
  URN =		{urn:nbn:de:0030-drops-162125},
  doi =		{10.4230/DARTS.8.2.14},
  annote =	{Keywords: Session Types, Rust, DSL}
}

Document

DOI: 10.4230/LIPIcs.ECOOP.2022.22

Ferrite: A Judgmental Embedding of Session Types in Rust

Authors: Ruo Fei Chen, Stephanie Balzer, and Bernardo Toninho

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

Abstract

Session types have proved viable in expressing and verifying the protocols of message-passing systems. While message passing is a dominant concurrency paradigm in practice, real world software is written without session types. A limitation of existing session type libraries in mainstream languages is their restriction to linear session types, precluding application scenarios that demand sharing and thus aliasing of channel references. This paper introduces Ferrite, a shallow embedding of session types in Rust that supports both linear and shared sessions. The formal foundation of Ferrite constitutes the shared session type calculus SILL_𝖲, which Ferrite encodes via a novel judgmental embedding technique. The fulcrum of the embedding is the notion of a typing judgment that allows reasoning about shared and linear resources to type a session. Typing rules are then encoded as functions over judgments, with a valid typing derivation manifesting as a well-typed Rust program. This Rust program generated by Ferrite serves as a certificate, ensuring that the application will proceed according to the protocol defined by the session type. The paper details the features and implementation of Ferrite and includes a case study on implementing Servo’s canvas component in Ferrite.

Cite as

Ruo Fei Chen, Stephanie Balzer, and Bernardo Toninho. Ferrite: A Judgmental Embedding of Session Types in Rust. In 36th European Conference on Object-Oriented Programming (ECOOP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 222, pp. 22:1-22:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{chen_et_al:LIPIcs.ECOOP.2022.22,
  author =	{Chen, Ruo Fei and Balzer, Stephanie and Toninho, Bernardo},
  title =	{{Ferrite: A Judgmental Embedding of Session Types in Rust}},
  booktitle =	{36th European Conference on Object-Oriented Programming (ECOOP 2022)},
  pages =	{22:1--22:28},
  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.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2022.22},
  URN =		{urn:nbn:de:0030-drops-162501},
  doi =		{10.4230/LIPIcs.ECOOP.2022.22},
  annote =	{Keywords: Session Types, Rust, DSL}
}

Search Results

Documents authored by Chen, Ruo Fei

Ferrite: A Judgmental Embedding of Session Types in Rust (Artifact)

Abstract

Cite as

Ferrite: A Judgmental Embedding of Session Types in Rust

Abstract

Cite as

Thanks for your feedback!

Could not send message