Ferrite: A Judgmental Embedding of Session Types in Rust

Ruo Fei Chen, Stephanie Balzer, Bernardo Toninho

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

1 Citation (Scopus)
13 Downloads (Pure)

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 SILLS, 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.

Original languageEnglish
Title of host publication36th European Conference on Object-Oriented Programming (ECOOP 2022)
EditorsKarim Ali, Jan Vitek
Place of PublicationWadern
PublisherSchloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
Number of pages28
ISBN (Print)978-3-95977-225-9
DOIs
Publication statusPublished - 23 Jun 2022
Event36th European Conference on Object-Oriented Programming, ECOOP 2022 - Berlin, Germany
Duration: 6 Jun 202210 Jun 2022

Publication series

NameLeibniz International Proceedings in Informatics, LIPIcs
PublisherSchloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
Volume222
ISSN (Print)1868-8969

Conference

Conference36th European Conference on Object-Oriented Programming, ECOOP 2022
Country/TerritoryGermany
CityBerlin
Period6/06/2210/06/22

Keywords

  • DSL
  • Rust
  • Session Types

Fingerprint

Dive into the research topics of 'Ferrite: A Judgmental Embedding of Session Types in Rust'. Together they form a unique fingerprint.

Cite this