scholarly journals Manifest Deadlock-Freedom for Shared Session Types

2019 ◽  
pp. 611-639 ◽  
Author(s):  
Stephanie Balzer ◽  
Bernardo Toninho ◽  
Frank Pfenning
Keyword(s):  
Session Types ◽  
Deadlock Freedom

scholarly journals Propositions as sessions

2014 ◽  
Vol 24 (2-3) ◽  
pp. 384-418 ◽  
Author(s):  
PHILIP WADLER
Keyword(s):  
Linear Functional ◽  
Linear Logic ◽  
Functional Language ◽  
Session Types ◽  
Deadlock Freedom ◽  
First Time ◽  
Standard Presentation

AbstractContinuing a line of work by Abramsky (1994), Bellin and Scott (1994), and Caires and Pfenning (2010), among others, this paper presents CP, a calculus, in which propositions of classical linear logic correspond to session types. Continuing a line of work by Honda (1993), Hondaet al. (1998), and Gay & Vasconcelos (2010), among others, this paper presents GV, a linear functional language with session types, and a translation from GV into CP. The translation formalises for the first time a connection between a standard presentation of session types and linear logic, and shows how a modification to the standard presentation yields a language free from races and deadlock, where race and deadlock freedom follows from the correspondence to linear logic.

scholarly journals Exploring Type-Level Bisimilarity towards More Expressive Multiparty Session Types

2020 ◽  
pp. 251-279 ◽  
Author(s):  
Sung-Shik Jongmans ◽  
Nobuko Yoshida
Keyword(s):  
Parallel Composition ◽  
Model Checker ◽  
Practical Result ◽  
Session Types ◽  
Deadlock Freedom ◽  
Algebraic Framework ◽  
A New Technique ◽  
Global Type ◽  
Existential Quantification ◽  
Process Algebraic

AbstractA key open problem with multiparty session types (MPST) concerns their expressiveness: current MPST have inflexible choice, no existential quantification over participants, and limited parallel composition. This precludes many real protocols to be represented by MPST. To overcome these bottlenecks of MPST, we explore a new technique using weak bisimilarity between global types and endpoint types, which guarantees deadlock-freedom and absence of protocol violations. Based on a process algebraic framework, we present well-formed conditions for global types that guarantee weak bisimilarity between a global type and its endpoint types and prove their check is decidable. Our main practical result, obtained through benchmarks, is that our well-formedness conditions can be checked orders of magnitude faster than directly checking weak bisimilarity using a state-of-the-art model checker.

An extensible approach to session polymorphism

2015 ◽  
Vol 26 (3) ◽  
pp. 465-509 ◽  
Author(s):  
MATTHEW GOTO ◽  
RADHA JAGADEESAN ◽  
ALAN JEFFREY ◽  
CORIN PITCHER ◽  
JAMES RIELY
Keyword(s):  
General Type ◽  
Type System ◽  
Input Output ◽  
Safety Properties ◽  
Session Types ◽  
Deadlock Freedom ◽  
Typing System ◽  
Limited Support ◽  
Session Type ◽  
Π Calculus

Session types describe and constrain the input/output behaviour of systems. Existing session typing systems have limited support for polymorphism. For example, existing systems cannot provide the most general type for a generic proxy process that forwards messages between two channels. We provide a polymorphic session typing system for the π calculus, and demonstrate the utility of session-type-level functions in combination with polymorphic session typing. The type system guarantees subject reduction and safety properties, but not deadlock freedom. We describe a formalization of the type system in Coq. The proofs of subject reduction and safety properties, as well as typing of example processes, have been mechanically verified.

Linear logic propositions as session types

2014 ◽  
Vol 26 (3) ◽  
pp. 367-423 ◽  
Author(s):  
LUÍS CAIRES ◽  
FRANK PFENNING ◽  
BERNARDO TONINHO
Keyword(s):  
Sequent Calculus ◽  
Linear Logic ◽  
Type System ◽  
Type Systems ◽  
Cut Elimination ◽  
Session Types ◽  
Deadlock Freedom ◽  
Session Type ◽  
Π Calculus ◽  
Intuitionistic Linear Logic

Throughout the years, several typing disciplines for the π-calculus have been proposed. Arguably, the most widespread of these typing disciplines consists of session types. Session types describe the input/output behaviour of processes and traditionally provide strong guarantees about this behaviour (i.e. deadlock-freedom and fidelity). While these systems exploit a fundamental notion of linearity, the precise connection between linear logic and session types has not been well understood.This paper proposes a type system for the π-calculus that corresponds to a standard sequent calculus presentation of intuitionistic linear logic, interpreting linear propositions as session types and thus providing a purely logical account of all key features and properties of session types. We show the deep correspondence between linear logic and session types by exhibiting a tight operational correspondence between cut-elimination steps and process reductions. We also discuss an alternative presentation of linear session types based on classical linear logic, and compare our development with other more traditional session type systems.

scholarly journals Embedding session types in Haskell

2018 ◽  
Vol 51 (12) ◽  
pp. 133-145 ◽  
Author(s):  
Sam Lindley ◽  
J. Garrett Morris
Keyword(s):  
Session Types

scholarly journals On Polymorphic Sessions and Functions

2021 ◽  
Vol 43 (2) ◽  
pp. 1-55
Author(s):  
Bernardo Toninho ◽  
Nobuko Yoshida
Keyword(s):  
Natural Deduction ◽  
Sequent Calculus ◽  
Linear Logic ◽  
Linear Formulation ◽  
Session Types ◽  
Logical Foundation ◽  
Π Calculus ◽  
Soundness And Completeness ◽  
System F ◽  
Algebraic Representations

This work exploits the logical foundation of session types to determine what kind of type discipline for the Λ-calculus can exactly capture, and is captured by, Λ-calculus behaviours. Leveraging the proof theoretic content of the soundness and completeness of sequent calculus and natural deduction presentations of linear logic, we develop the first mutually inverse and fully abstract processes-as-functions and functions-as-processes encodings between a polymorphic session π-calculus and a linear formulation of System F. We are then able to derive results of the session calculus from the theory of the Λ-calculus: (1) we obtain a characterisation of inductive and coinductive session types via their algebraic representations in System F; and (2) we extend our results to account for value and process passing, entailing strong normalisation.

Sign in / Sign up

Export Citation Format

Share Document