Honesty by typing

Massimo Bartoletti; Alceste Scalas; Emilio Tuosto; Roberto Zunino; Alexandra Silva

doi:10.2168/LMCS-12(4:7)2016

Honesty by typing

Massimo Bartoletti, Alceste Scalas, Emilio Tuosto, Roberto Zunino, Alexandra Silva (Editor)

College of Engineering and Physical Sciences

Research output: Contribution to journal › Article › peer-review

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.

Original language	English
Pages (from-to)	1-58
Journal	Logical Methods in Computer Science
Volume	12
Issue number	4:7
DOIs	https://doi.org/10.2168/LMCS-12(4:7)2016
Publication status	Published - 28 Dec 2016

Bibliographical note

©M. Bartoletti, A. Scalas, E. Tuosto, and R. Zunino

CC Creative Commons

Access to Document

10.2168/LMCS-12(4:7)2016Licence: CC BY 3.0

HONESTY BY TYPING
©M. Bartoletti, A. Scalas, E. Tuosto, and R. Zunino CC Creative Commons
Final published version, 707 KBLicence: CC BY 3.0

Cite this

@article{29956e889c66470fa229981ce47a1ee8,

title = "Honesty by typing",

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.",

author = "Massimo Bartoletti and Alceste Scalas and Emilio Tuosto and Roberto Zunino and Alexandra Silva",

note = "{\textcopyright}M. Bartoletti, A. Scalas, E. Tuosto, and R. Zunino CC Creative Commons",

year = "2016",

month = dec,

day = "28",

doi = "10.2168/LMCS-12(4:7)2016",

language = "English",

volume = "12",

pages = "1--58",

journal = "Logical Methods in Computer Science",

issn = "1860-5974",

publisher = "Technischen Universitat Braunschweig",

number = "4:7",

}

TY - JOUR

T1 - Honesty by typing

AU - Bartoletti, Massimo

AU - Scalas, Alceste

AU - Tuosto, Emilio

AU - Zunino, Roberto

A2 - Silva, Alexandra

PY - 2016/12/28

Y1 - 2016/12/28

N2 - 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.

AB - 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.

UR - https://lmcs.episciences.org/2619

U2 - 10.2168/LMCS-12(4:7)2016

DO - 10.2168/LMCS-12(4:7)2016

M3 - Article

SN - 1860-5974

VL - 12

SP - 1

EP - 58

JO - Logical Methods in Computer Science

JF - Logical Methods in Computer Science

IS - 4:7

ER -

Honesty by typing

Abstract

Bibliographical note

Access to Document

Other files and links

Fingerprint

Cite this