Linearity, session types and the pi calculus

DOI10.1017/S0960129514000176MaRDI QIDQ5741562zbMATH OpenFDO

Authors Marco Giunti, Vasco T. Vasconcelos

Publication date 28 July 2016

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

Full work available at URL https://doi.org/10.1017/S0960129514000176

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)

Recommendations

• A linear account of session types in the pi calculus
• Session types as intuitionistic linear propositions
• Fundamentals of session types
• Linear logic propositions as session types
• Subtyping for session types in the pi calculus

Cites work

• A calculus of mobile processes. I
• A linear account of session types in the pi calculus
• Amalgamating sessions and methods in object-oriented languages with generics
• Asynchronous Session Types and Progress for Object Oriented Languages
• Bounded Session Types for Object Oriented Languages
• Conversation types
• Functions as processes
• Fundamentals of session types
• Linear type theory for asynchronous session types
• On projecting processes into session types
• Subtyping for session types in the pi calculus
• Type checking a multithreaded functional language with session types

Cited in

(16)

• \( \pi\) with leftovers: a mechanisation in Agda
• Session typing and asynchronous subtyping for the higher-order \(\pi\)-calculus
• Session types revisited
• Algorithmic type checking for a pi-calculus with name matching and session types
• Subtyping for session types in the pi calculus
• On projecting processes into session types
• Linearity, control effects, and behavioral types
• Full abstraction in a subtyped pi-calculus with linear types
• Context-free session types for applied pi-calculus
• Session types as intuitionistic linear propositions
• A linear account of session types in the pi calculus
• Session types as generic process types
• A universal session type for untyped asynchronous communication
• Type reconstruction for the linear -calculus with composite and equi-recursive types
• Linear logic propositions as session types
• Fundamentals of session types

This page was built for publication: Linearity, session types and the pi calculus

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5741562)