Honesty by Typing

TL;DR

This paper introduces a type system for a process calculus that guarantees honesty in contractual interactions, ensuring processes adhere to their stipulated contracts even amidst dishonest adversaries, with decidable type inference for both communication modes.

Contribution

It presents a novel type system that guarantees honesty in process interactions and provides a decidable type inference method for both synchronous and asynchronous communication.

Findings

Type safety guarantees honesty in process interactions.

Type inference is decidable for both communication modes.

Processes are proven to abide by contracts in all contexts.

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.