Type checking a multithreaded functional language with session types

DOI10.1016/j.tcs.2006.06.028zbMath1171.68410OpenAlexW2105716349MaRDI QIDQ859841

António Ravara, Simon J. Gay, Vasco Thudichum Vasconcelos

Publication date: 22 January 2007

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.tcs.2006.06.028

zbMATH Keywords

concurrent programmingsession typesspecification of communication protocolsstatic type checking

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items (20)

On projecting processes into session types ⋮ Relating Functional and Imperative Session Types ⋮ Session types revisited ⋮ Combining behavioural types with security analysis ⋮ Separating Sessions Smoothly ⋮ Bounded polymorphism in session types ⋮ Deriving session and union types for objects ⋮ Linearity, session types and the Pi calculus ⋮ An extensible approach to session polymorphism ⋮ Asynchronous Session Types and Progress for Object Oriented Languages ⋮ Linear type theory for asynchronous session types ⋮ Amalgamating sessions and methods in object-oriented languages with generics ⋮ The stream-based service-centred calculus: a foundation for service-oriented programming ⋮ Session Types with Gradual Typing ⋮ Objects and session types ⋮ Parameterised notions of computation ⋮ 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 ⋮ Prioritise the best variation

Uses Software

• ML
• Haskell
• Cyclone
• PIPER

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• The lambda calculus. Its syntax and semantics. Rev. ed.
• A calculus of mobile processes. II
• A theory of type polymorphism in programming
• Typing correspondence assertions for communication protocols
• A generic type system for the pi-calculus
• Subtyping for session types in the pi calculus
• Bounded Session Types for Object Oriented Languages
• Correspondence assertions for process synchronization in concurrent communications
• Types as models
• Resource usage analysis
• CONCUR 2004 - Concurrency Theory
• Trustworthy Global Computing

This page was built for publication: Type checking a multithreaded functional language with session types