Type Inference for Session Types in the $$\pi $$ -calculus

2016 ◽  
pp. 103-121 ◽  
Author(s):  
Eva Fajstrup Graversen ◽  
Jacob Buchreitz Harbo ◽  
Hans Hüttel ◽  
Mathias Ormstrup Bjerregaard ◽  
Niels Sonnich Poulsen ◽  
...  
Keyword(s):  
Type Inference ◽  
Session Types ◽  
Pi Calculus

A simple library implementation of binary sessions

2016 ◽  
Vol 27 ◽  
Author(s):  
LUCA PADOVANI
Keyword(s):  
Programming Language ◽  
Protocol Analysis ◽  
Simple Approach ◽  
Type Inference ◽  
Hybrid Form ◽  
Type Checking ◽  
Session Types ◽  
Parametric Polymorphism ◽  
Session Type

AbstractInspired by the continuation-passing encoding of binary sessions, we describe a simple approach to embed a hybrid form of session type checking into any programming language that supports parametric polymorphism. The approach combines static protocol analysis with dynamic linearity checks. To demonstrate the effectiveness of the technique, we implement a well-integrated OCaml module for session communications. For free, OCaml provides us with equirecursive session types, parametric behavioural polymorphism, complete session type inference, and session subtyping.

scholarly journals Linearity, session types and the Pi calculus

2014 ◽  
Vol 26 (2) ◽  
pp. 206-237 ◽  
Author(s):  
MARCO GIUNTI ◽  
VASCO THUDICHUM VASCONCELOS
Keyword(s):  
Communication Channel ◽  
Type System ◽  
Type Systems ◽  
Session Types ◽  
Completeness Result ◽  
Pi Calculus

We present a type system based on session types that works on a conventional pi calculus. Types are equipped with a constructor that describes the two ends of a single communication channel, this being the only type available for describing the behaviour of channels. Session types, in turn, describe the behaviour of each individual channel end, as usual. A novel notion of typing context split allows for typing processes not typable with extant type systems. We show that our system guarantees that typed processes do not engage in races for linear resources. We assess the expressiveness of the type system by providing three distinct encodings – from the pi calculus with polarized variables, from the pi calculus with accept and request primitives, and from the linear pi calculus – into our system. For each language we present operational and typing correspondences, showing that our system effectively subsumes foregoing works on linear and session types. In the case of the linear pi calculus we also provide a completeness result.

scholarly journals Using session types for reasoning about boundedness in the $$\pi $$-calculus

2019 ◽  
Vol 57 (6) ◽  
pp. 801-827
Author(s):  
Hans Hüttel
Keyword(s):  
Session Types ◽  
Pi Calculus

scholarly journals Bounded polymorphism in session types

2008 ◽  
Vol 18 (5) ◽  
pp. 895-930 ◽  
Author(s):  
SIMON J. GAY
Keyword(s):  
Operational Semantics ◽  
Client Server ◽  
Session Types ◽  
Patterns Of Communication ◽  
Pi Calculus ◽  
Run Time ◽  
High Level ◽  
Communication Errors

Session types allow high-level specifications of structured patterns of communication, such as client-server protocols, to be expressed as types and verified by static typechecking. In collaboration with Malcolm Hole, we previously introduced a notion of subtyping for session types, which was formulated for an extended pi calculus. Subtyping allows one part of a system, for example, a server, to be refined without invalidating type-correctness of other parts, for example, clients. In this paper we introduce bounded polymorphism, which is based on the same notion of subtyping, in order to support more precise and flexible specifications of protocols; in particular, a choice of type in one message may affect the types of future messages. We formalise the syntax, operational semantics and typing rules of an extended pi calculus, and prove that typechecking guarantees the absence of run-time communication errors. We study algorithms for checking instances of the subtype relation in two versions of our system, which we call KernelS≤and FullS≤, and establish that subtyping in KernelS≤is decidable, and that subtyping in FullS≤is undecidable.

scholarly journals Context-Free Session Types for Applied Pi-Calculus

2018 ◽  
Vol 276 ◽  
pp. 3-18
Author(s):  
Jens Aagaard ◽  
Hans Hüttel ◽  
Mathias Jakobsen ◽  
Mikkel Kettunen
Keyword(s):  
Session Types ◽  
Pi Calculus ◽  
Context Free

Subtyping for session types in the pi calculus

2005 ◽  
Vol 42 (2-3) ◽  
pp. 191-225 ◽  
Author(s):  
Simon Gay ◽  
Malcolm Hole
Keyword(s):  
Session Types ◽  
Pi Calculus

A Distributed Pi-Calculus

2007 ◽  
Author(s):  
Matthew Hennessy
Keyword(s):  
Pi Calculus
Sign in / Sign up

Export Citation Format

Share Document