一句话：提出面向契约进程演算的类型系统，保证可类型化进程在所有上下文中诚实，并给出可判定的类型推断。
论文研究契约进程中的诚实性（honesty）问题：进程通过契约建立会话，可能在交互中遵守或不遵守承诺。作者提出一个类型系统，对契约进程演算进行静态分析，证明类型安全蕴含诚实性，即只要进程可类型化，它在所有可能上下文中（即使面对不诚实对手）都会履行已订立的契约。方法上设计了类型规则并证明类型推断可判定，可用同步或异步通信语义安全地近似诚实性。关键结果是类型系统保证诚实性且推断可自动化，为会话契约的可信交互提供形式化基础。
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.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{abs-1211-2609,
title = {Honesty by Typing},
author = {Massimo Bartoletti and Alceste Scalas and Emilio Tuosto and Roberto Zunino},
journal = {Logical Methods in Computer Science},
volume = {Volume 12, Issue 4},
year = {2017},
doi = {10.2168/lmcs-12(4:7)2016}
}