Ankush Das ; Frank Pfenning - Rast: A Language for Resource-Aware Session Types

lmcs:7024 - Logical Methods in Computer Science, January 12, 2022, Volume 18, Issue 1 - https://doi.org/10.46298/lmcs-18(1:9)2022
Rast: A Language for Resource-Aware Session TypesArticle

Authors: Ankush Das ; Frank Pfenning

    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.


    Volume: Volume 18, Issue 1
    Published on: January 12, 2022
    Accepted on: October 29, 2021
    Submitted on: December 25, 2020
    Keywords: Computer Science - Programming Languages,Computer Science - Logic in Computer Science
    Funding:
      Source : OpenAIRE Graph
    • SaTC: CORE: Medium: Collaborative: Automated Support for Writing High-Assurance Smart Contracts; Funder: National Science Foundation; Code: 1801369
    • CAREER: Marlin: A Unified Framework for Automatic and Interactive Quantitative Program Analysis; Funder: National Science Foundation; Code: 1845514

    1 Document citing this article

    Consultation statistics

    This page has been seen 1736 times.
    This article's PDF has been downloaded 722 times.