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.

Honesty by typing

BARTOLETTI, MASSIMO;SCALAS, ALCESTE;
2016-01-01

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.
2016
Computer science; Programming languages
File in questo prodotto:
File Dimensione Formato  
HbT.pdf

Solo gestori archivio

Descrizione: Articolo principale
Tipologia: versione pre-print
Dimensione 698.95 kB
Formato Adobe PDF
698.95 kB Adobe PDF   Visualizza/Apri   Richiedi una copia

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11584/216068
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 9
  • ???jsp.display-item.citation.isi??? 8
social impact