Type-Based Analysis for Session Inference (Extended Abstract)

DOI10.1007/978-3-319-39570-8_17zbMATH Open1347.68057arXiv1510.03929OpenAlexW2463705546MaRDI QIDQ2827469FDOQ2827469

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)

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.

Full work available at URL: https://arxiv.org/abs/1510.03929

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

Mathematics Subject Classification ID

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

Cites Work

• Subtyping for session types in the pi calculus
• Session types as intuitionistic linear propositions
• Linear type theory for asynchronous session types
• Propositions as sessions
• Title not available (Why is that?)
• 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.
• Higher-order processes, functions, and sessions: a monadic integration
• Type reconstruction for the linear \(\pi\)-calculus with composite regular types

Cited In (4)

• Behavioural analysis of sessions using the calculus of structures
• Information flow inference for ML
• Type checking a multithreaded functional language with session types
• Context-free session type inference

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)