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.CONCUR.2020.13
URN: urn:nbn:de:0030-drops-128252
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2020/12825/
Go to the corresponding LIPIcs Volume Portal

Das, Ankush ; Pfenning, Frank

Session Types with Arithmetic Refinements

pdf-format:
LIPIcs-CONCUR-2020-13.pdf (0.5 MB)

Abstract

Session types statically prescribe bidirectional communication protocols for message-passing processes. However, simple session types cannot specify properties beyond the type of exchanged messages. In this paper we extend the type system by using index refinements from linear arithmetic capturing intrinsic attributes of data structures and algorithms. We show that, despite the decidability of Presburger arithmetic, type equality and therefore also subtyping and type checking are now undecidable, which stands in contrast to analogous dependent refinement type systems from functional languages. We also present a practical, but incomplete algorithm for type equality, which we have used in our implementation of Rast, a concurrent session-typed language with arithmetic index refinements as well as ergometric and temporal types. Moreover, if necessary, the programmer can propose additional type bisimulations that are smoothly integrated into the type equality algorithm.

BibTeX - Entry

@InProceedings{das_et_al:LIPIcs:2020:12825,
  author =	{Ankush Das and Frank Pfenning},
  title =	{{Session Types with Arithmetic Refinements}},
  booktitle =	{31st International Conference on Concurrency Theory (CONCUR 2020)},
  pages =	{13:1--13:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-160-3},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{171},
  editor =	{Igor Konnov and Laura Kov{\'a}cs},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2020/12825},
  URN =		{urn:nbn:de:0030-drops-128252},
  doi =		{10.4230/LIPIcs.CONCUR.2020.13},
  annote =	{Keywords: Session Types, Refinement Types, Type Equality}
}

Keywords: Session Types, Refinement Types, Type Equality
Collection: 31st International Conference on Concurrency Theory (CONCUR 2020)
Issue Date: 2020
Date of publication: 26.08.2020

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