Intersections and Unions of Session Types

Intersections and Unions of Session Types

Prior work has extended the deep, logical connection between the linear sequent calculus and session-typed message-passing concurrent computation with equi-recursive types and a natural notion of subtyping. In this paper, we extend this further by intersection and union types in order to express mul...

Full description

Bibliographic Details
Main Authors: Coşku Acay, Frank Pfenning
Format: Article
Language:English
Published: Open Publishing Association 2017-02-01
Series:Electronic Proceedings in Theoretical Computer Science
Online Access:http://arxiv.org/pdf/1702.02272v1
id doaj-0f14cbdc0cd14876ae45f534d5d79ffb
record_format Article
spelling doaj-0f14cbdc0cd14876ae45f534d5d79ffb2020-11-24T23:41:31ZengOpen Publishing AssociationElectronic Proceedings in Theoretical Computer Science2075-21802017-02-01242Proc. ITRS 201641910.4204/EPTCS.242.3:4Intersections and Unions of Session TypesCoşku Acay0Frank Pfenning1 Carnegie Mellon University Carnegie Mellon University Prior work has extended the deep, logical connection between the linear sequent calculus and session-typed message-passing concurrent computation with equi-recursive types and a natural notion of subtyping. In this paper, we extend this further by intersection and union types in order to express multiple behavioral properties of processes in a single type. We prove session fidelity and absence of deadlock and illustrate the expressive power of our system with some simple examples. We observe that we can represent internal and external choice by intersection and union, respectively, which was previously suggested by Padovani for a different language of session types motivated by operational rather than logical concerns.http://arxiv.org/pdf/1702.02272v1
collection DOAJ
language English
format Article
sources DOAJ
author Coşku Acay
Frank Pfenning
spellingShingle Coşku Acay
Frank Pfenning
Intersections and Unions of Session Types
Electronic Proceedings in Theoretical Computer Science
author_facet Coşku Acay
Frank Pfenning
author_sort Coşku Acay
title Intersections and Unions of Session Types
title_short Intersections and Unions of Session Types
title_full Intersections and Unions of Session Types
title_fullStr Intersections and Unions of Session Types
title_full_unstemmed Intersections and Unions of Session Types
title_sort intersections and unions of session types
publisher Open Publishing Association
series Electronic Proceedings in Theoretical Computer Science
issn 2075-2180
publishDate 2017-02-01
description Prior work has extended the deep, logical connection between the linear sequent calculus and session-typed message-passing concurrent computation with equi-recursive types and a natural notion of subtyping. In this paper, we extend this further by intersection and union types in order to express multiple behavioral properties of processes in a single type. We prove session fidelity and absence of deadlock and illustrate the expressive power of our system with some simple examples. We observe that we can represent internal and external choice by intersection and union, respectively, which was previously suggested by Padovani for a different language of session types motivated by operational rather than logical concerns.
url http://arxiv.org/pdf/1702.02272v1
work_keys_str_mv AT coskuacay intersectionsandunionsofsessiontypes
AT frankpfenning intersectionsandunionsofsessiontypes
_version_ 1725506935627710464

Similar Items