Document Open Access Logo

Minimal Session Types (Pearl)

Authors Alen Arslanagić , Jorge A. Pérez , Erik Voogd



PDF
Thumbnail PDF

File

LIPIcs.ECOOP.2019.23.pdf
  • Filesize: 0.65 MB
  • 28 pages

Document Identifiers

Author Details

Alen Arslanagić
  • University of Groningen, The Netherlands
Jorge A. Pérez
  • University of Groningen, The Netherlands
Erik Voogd
  • University of Groningen, The Netherlands

Acknowledgements

We are grateful to the anonymous reviewers for their remarks and questions. Pérez is also with CWI, Amsterdam and NOVA LINCS - the NOVA Laboratory for Computer Science and Informatics, Universidade Nova de Lisboa, Portugal (Ref. UID/CEC/04516/2019).

Cite AsGet BibTex

Alen Arslanagić, Jorge A. Pérez, and Erik Voogd. Minimal Session Types (Pearl). In 33rd European Conference on Object-Oriented Programming (ECOOP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 134, pp. 23:1-23:28, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2019)
https://doi.org/10.4230/LIPIcs.ECOOP.2019.23

Abstract

Session types are a type-based approach to the verification of message-passing programs. They have been much studied as type systems for the pi-calculus and for languages such as Java. A session type specifies what and when should be exchanged through a channel. Central to session-typed languages are constructs in types and processes that specify sequencing in protocols. Here we study minimal session types, session types without sequencing. This is arguably the simplest form of session types. By relying on a core process calculus with sessions and higher-order concurrency (abstraction-passing), we prove that every process typable with standard (non minimal) session types can be compiled down into a process typed with minimal session types. This means that having sequencing constructs in both processes and session types is redundant; only sequentiality in processes is indispensable, as it can precisely codify sequentiality in types. Our developments draw inspiration from work by Parrow on behavior-preserving decompositions of untyped processes. By casting Parrow’s results in the realm of typed processes, our results reveal a conceptually simple formulation of session types and a principled avenue to the integration of session types into languages without sequencing in types.

Subject Classification

ACM Subject Classification
  • Theory of computation → Type structures
  • Theory of computation → Process calculi
  • Software and its engineering → Concurrent programming structures
  • Software and its engineering → Message passing
Keywords
  • Session types
  • process calculi
  • pi-calculus

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail