Rast: A Language for Resource-Aware Session Types

TL;DR

Rast is a language that extends session types with arithmetic refinements, temporal types, and polymorphism to specify and verify resource usage and complexity bounds in concurrent programs.

Contribution

It introduces Rast, an open-source language combining session types with resource-aware refinements, temporal types, and polymorphism, along with an optimized type checking and reconstruction engine.

Findings

Supports resource and complexity analysis in session-typed programs

Demonstrates expressivity through various examples

Provides an open-source implementation with automated type reconstruction

Abstract

Traditional session types prescribe bidirectional communication protocols for concurrent computations, where well-typed programs are guaranteed to adhere to the protocols. However, simple session types cannot capture properties beyond the basic type of the exchanged messages. In response, recent work has extended session types with refinements from linear arithmetic, capturing intrinsic attributes of processes and data. These refinements then play a central role in describing sequential and parallel complexity bounds on session-typed programs. The Rast language provides an open-source implementation of session-typed concurrent programs extended with arithmetic refinements as well as ergometric and temporal types to capture work and span of program execution. To further support generic programming, Rast also enhances arithmetically refined session types with recently developed nested parametric polymorphism. Type checking relies on Cooper's algorithm for quantifier elimination in Presburger arithmetic with a few significant optimizations, and a heuristic extension to nonlinear constraints. Rast furthermore includes a reconstruction engine so that most program constructs pertaining the layers of refinements and resources are inserted automatically. We provide a variety of examples to demonstrate the expressivity of the language.