A Predicate Transformer for Choreographies (Technical Report)

This technical report contains detailed definitions, auxiliary lemmas, main theorems, and proofs related to the paper A Predicate Transformer for Choreographies, published in the proceedings of ESOP 2022. The aim of this document is to provide a comprehensive reference guide for the theory presented in the paper. In contrast to the paper, we do not split the presentation into a base calculus, an extension with blocking if/while-statements, and an extension with non-blocking if/while statements. Instead, we present the whole calculus of global programs, including all extensions, at once.