Honesty by typing


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.

Publication DOI: https://doi.org/10.2168/LMCS-12(4:7)2016
Divisions: College of Engineering & Physical Sciences
Additional Information: ©M. Bartoletti, A. Scalas, E. Tuosto, and R. Zunino CC Creative Commons
Publication ISSN: 1860-5974
Last Modified: 10 Jun 2024 07:34
Date Deposited: 18 Jun 2019 08:51
Full Text Link:
Related URLs: https://lmcs.ep ... iences.org/2619 (Publisher URL)
PURE Output Type: Article
Published Date: 2016-12-28
Accepted Date: 2016-04-02
Authors: Bartoletti, Massimo
Scalas, Alceste (ORCID Profile 0000-0002-1153-6164)
Tuosto, Emilio
Zunino, Roberto



Version: Published Version

License: Creative Commons Attribution

| Preview

Export / Share Citation


Additional statistics for this record