Honesty by typing

DOI10.2168/LMCS-12(4:7)2016MaRDI QIDQ2974791zbMATH OpenFDO

Authors Massimo Bartoletti, Alceste Scalas, Roberto Zunino, Emilio Tuosto

Publication date 11 April 2017

Published in Logical Methods in Computer Science (Search for Journal in Brave)

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

zbMATH Keywords

contract-oriented computingsession typesverification

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Abstract: We propose a type system for a calculus of contracting processes. Processes can establish sessions by stipulating contracts, and then can interact either by keeping the promises made, or not. Type safety guarantees that a typeable process is honest - that is, it abides by the contracts it has stipulated in all possible contexts, even in presence of dishonest adversaries. Type inference is decidable, and it allows to safely approximate the honesty of processes using either synchronous or asynchronous communication.

Recommendations

• On the realizability of contracts in dishonest systems
• Session-typed concurrent contracts
• Session-typed concurrent contracts
• Contracts for Mobile Processes
• Verifiable abstractions for contract-oriented systems

Cites work

• A finite equational base for CCS with left merge and communication merge
• A New Type System for Deadlock-Free Processes
• A semantic deconstruction of session types
• An Algorithm for the General Petri Net Reachability Problem
• Compliance and subtyping in timed session types
• Compliance in behavioural contracts: a brief survey
• From communicating machines to graphical choreographies
• Fundamentals of session types
• Global progress for dynamically interleaved multiparty sessions
• Global Progress in Dynamically Interleaved Multiparty Sessions
• Honesty by typing
• scientific article; zbMATH DE number 1263840 (Why is no real title available?)
• scientific article; zbMATH DE number 1059894 (Why is no real title available?)
• scientific article; zbMATH DE number 1456956 (Why is no real title available?)
• Multiparty asynchronous session types
• Multiparty compatibility in communicating automata: characterisation and synthesis of global session types
• On Communicating Finite-State Machines
• On the realizability of contracts in dishonest systems
• Sub-behaviour relations for session-based client/server systems
• Synthesising Choreographies from Local Session Types
• Timed runtime monitoring for multiparty conversations
• Using higher-order contracts to model session types (extended abstract)
• Verifiable abstractions for contract-oriented systems
• Verification of programs with half-duplex communication
• Verifying identical communicating processes is undecidable

Cited in

(12)

• A fixed-points based framework for compliance of behavioural contracts
• On the realizability of contracts in dishonest systems
• Modelling and verifying contract-oriented systems in Maude
• Honesty by typing
• On the undecidability of asynchronous session subtyping
• Honesty through repeated interactions
• Contracts for Mobile Processes
• Verifiable abstractions for contract-oriented systems
• Session-typed concurrent contracts
• Declarative choreographies and liveness
• MAG\(\pi\): types for failure-prone communication
• On asynchronous multiparty session types for federated learning

Describes a project that uses

Uses Software

• BetaSim
• BETA
• Diogenes

This page was built for publication: Honesty by typing

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