Type-Based Analysis for Session Inference (Extended Abstract)

DOI10.1007/978-3-319-39570-8_17MaRDI QIDQ2827469zbMATH OpenOpenAlexFDO

Authors Carlo Spaccasassi, Vasileios Koutavas

Publication date 19 October 2016

Published in Formal Techniques for Distributed Objects, Components, and Systems (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1510.03929, https://hal.inria.fr/hal-01432922/file/426757_1_En_17_Chapter.pdf

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19)

Abstract: We propose a type-based analysis to infer the session protocols of channels in an ML-like concurrent functional language. Combining and extending well-known techniques, we develop a type-checking system that separates the underlying ML type system from the typing of sessions. Without using linearity, our system guarantees communication safety and partial lock freedom. It also supports provably complete session inference for finite sessions with no programmer annotations. We exhibit the usefulness of our system with interesting examples, including one which is not typable in substructural type systems.

Recommendations

• Context-free session type inference
• A semantic deconstruction of session types
• Session types as intuitionistic linear propositions
• On the preciseness of subtyping in session types
• Typing the behavior of software components using session types
• Context-free session types
• Deciding the bisimilarity of context-free session types

Cites work

• scientific article; zbMATH DE number 1398002 (Why is no real title available?)
• Higher-order processes, functions, and sessions: a monadic integration
• Linear type theory for asynchronous session types
• Propositions as sessions
• Session types as intuitionistic linear propositions
• Subtyping for session types in the pi calculus
• Type and behaviour reconstruction for higher-order concurrent programs
• Type checking a multithreaded functional language with session types
• Type reconstruction for linear \(\pi\)-calculus with I/O subtyping.
• Type reconstruction for the linear \(\pi\)-calculus with composite regular types

Cited in

(5)

• Context-free session type inference
• Behavioural analysis of sessions using the calculus of structures
• Information flow inference for ML
• Type checking a multithreaded functional language with session types
• Inference Systems with Corules for Combined Safety and Liveness Properties of Binary Session Types

This page was built for publication: Type-Based Analysis for Session Inference (Extended Abstract)

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