Linear type theory for asynchronous session types

DOI10.1017/S0956796809990268zbMath1185.68194OpenAlexW2124126159MaRDI QIDQ5189644

Simon J. Gay, Vasco Thudichum Vasconcelos

Publication date: 17 March 2010

Published in: Journal of Functional Programming (Search for Journal in Brave)

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

zbMATH Keywords

multithreaded functional language with session typesstructured patterns of communication

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Semantics in the theory of computing (68Q55)

Related Items (43)

Characteristic bisimulation for higher-order session processes ⋮ Mixed Sessions ⋮ Behavioural Analysis of Sessions Using the Calculus of Structures ⋮ Back to futures ⋮ I Got Plenty o’ Nuttin’ ⋮ Linear $$ \lambda \mu $$ is $$ \textsc {CP} $$ (more or less) ⋮ Verifiable abstractions for contract-oriented systems ⋮ Fairness and communication-based semantics for session-typed languages ⋮ Separating Sessions Smoothly ⋮ Polarized subtyping ⋮ Algorithmic type checking for a pi-calculus with name matching and session types ⋮ A simple library implementation of binary sessions ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Observed Communication Semantics for Classical Processes ⋮ Linearity, Control Effects, and Behavioral Types ⋮ Context-Free Session Type Inference ⋮ A Higher-Order Logic for Concurrent Termination-Preserving Refinement ⋮ Unnamed Item ⋮ A WSDL-based type system for asynchronous WS-BPEL processes ⋮ Linearity, session types and the Pi calculus ⋮ On asynchronous eventful session semantics ⋮ An extensible approach to session polymorphism ⋮ Fundamentals of session types ⋮ On the relative expressiveness of higher-order session processes ⋮ Unnamed Item ⋮ A message-passing interpretation of adjoint logic ⋮ On the Relative Expressiveness of Higher-Order Session Processes ⋮ Amalgamating sessions and methods in object-oriented languages with generics ⋮ Typing Copyless Message Passing ⋮ Session Types with Gradual Typing ⋮ Corecursion and Non-divergence in Session-Typed Processes ⋮ Mixed sessions ⋮ Session-Based Communication Optimisation for Higher-Order Mobile Processes ⋮ Session Types with Arithmetic Refinements ⋮ Type-Based Analysis for Session Inference (Extended Abstract) ⋮ Session typing and asynchronous subtyping for the higher-order \(\pi\)-calculus ⋮ Polymorphic lambda calculus with context-free session types ⋮ Propositions as sessions ⋮ Prioritise the best variation ⋮ \( \pi\) with leftovers: a mechanisation in Agda

Cites Work

• Type checking a multithreaded functional language with session types
• Amalgamating sessions and methods in object-oriented languages with generics
• A syntactic approach to type soundness
• Subtyping for session types in the pi calculus
• Bounded polymorphism in session types
• Correspondence assertions for process synchronization in concurrent communications
• Asynchronous Session Types and Progress for Object Oriented Languages

This page was built for publication: Linear type theory for asynchronous session types