A Predicate Transformer for Choreographies (Technical Report)

Sung-Shik Jongmans*, Petra van den Bos

*Corresponding author for this work

Research output: Book/ReportTechnical reportAcademic

26 Downloads (Pure)


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.
Original languageEnglish
Place of PublicationHeerlen
PublisherOpen Universiteit Nederland
Number of pages132
Publication statusPublished - 2022

Publication series

SeriesOUNL-CS (Technical Reports)

Cite this