An extensible approach to session polymorphism

DOI10.1017/S0960129514000231zbMath1361.68168MaRDI QIDQ5741569

Matthew Goto, Corin Pitcher, Radha Jagadeesan, Alan Jeffrey, James Riely

Publication date: 28 July 2016

Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Related Items (2)

Polymorphic lambda calculus with context-free session types ⋮ \( \pi\) with leftovers: a mechanisation in Agda

Uses Software

• Coq

Cites Work

• Trace-based verification of imperative programs with I/O
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Type checking a multithreaded functional language with session types
• A calculus of mobile processes. I
• \(\pi\)-calculus in (Co)inductive-type theory
• The locally nameless representation
• Subtyping for session types in the pi calculus
• A Coq Library for Verification of Concurrent Programs
• Bounded polymorphism in session types
• Session Types as Intuitionistic Linear Propositions
• Correspondence assertions for process synchronization in concurrent communications
• Linear type theory for asynchronous session types
• Behavioral Polymorphism and Parametricity in Session-Based Communication
• Asynchronous Session Types and Progress for Object Oriented Languages
• A New Type System for Deadlock-Free Processes

This page was built for publication: An extensible approach to session polymorphism