# Intersections and Unions of Session Types

## TL;DR

This paper extends session types with intersection and union types to better express multiple behavioral properties of processes, proving key properties like session fidelity and deadlock freedom, and illustrating their expressive power.

## Contribution

It introduces intersection and union types into session-typed calculi, enhancing expressiveness and providing formal proofs of correctness properties.

## Key findings

- Representation of internal and external choice using intersection and union
- Proofs of session fidelity and deadlock freedom
- Demonstration of increased expressive power

## Abstract

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.