License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.FSCD.2020.33
URN: urn:nbn:de:0030-drops-123558
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2020/12355/
Go to the corresponding LIPIcs Volume Portal

Das, Ankush ; Pfenning, Frank

Rast: Resource-Aware Session Types with Arithmetic Refinements (System Description)

pdf-format:
LIPIcs-FSCD-2020-33.pdf (0.5 MB)

Abstract

Traditional session types prescribe bidirectional communication protocols for concurrent computations, where well-typed programs are guaranteed to adhere to the protocols. Recent work has extended session types with refinements from linear arithmetic, capturing intrinsic properties 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 and system provide 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. 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.

BibTeX - Entry

@InProceedings{das_et_al:LIPIcs:2020:12355,
  author =	{Ankush Das and Frank Pfenning},
  title =	{{Rast: Resource-Aware Session Types with Arithmetic Refinements (System Description)}},
  booktitle =	{5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)},
  pages =	{33:1--33:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-155-9},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{167},
  editor =	{Zena M. Ariola},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2020/12355},
  URN =		{urn:nbn:de:0030-drops-123558},
  doi =		{10.4230/LIPIcs.FSCD.2020.33},
  annote =	{Keywords: Session Types, Resource Analysis, Refinement Types}
}

Keywords: Session Types, Resource Analysis, Refinement Types
Collection: 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)
Issue Date: 2020
Date of publication: 28.06.2020
Supplementary Material: https://bitbucket.org/fpfenning/rast/src/master/rast/

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI