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.
Maurizio Murgia, 2021, A fixed-points based framework for compliance of behavioural contracts, Journal of Logical and Algebraic Methods in Programming, 120, pp. 100641, 10.1016/j.jlamp.2021.100641.
Alceste Scalas;Nobuko Yoshida, 2019, Less is more: multiparty session types revisited, Proceedings of the ACM on Programming Languages, 3, POPL, pp. 1-29, 10.1145/3290343, https://doi.org/10.1145/3290343.