Honesty by Typing
classification
💻 cs.PL
keywords
processestypecontractseitherhonestyabidesadversariesallows
pith:TEHWC3MQ Add to your LaTeX paper
What is a Pith Number?\usepackage{pith}
\pithnumber{TEHWC3MQ}
Prints a linked pith:TEHWC3MQ badge after your title and writes the identifier into PDF metadata. Compiles on arXiv with no extra files. Learn more
read the original 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.
This paper has not been read by Pith yet.
discussion (0)
Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.