A Predicate Transformer for Choreographies - Computing Preconditions in Choreographic Programming.

Sung-Shik Jongmans, Petra van den Bos

Research output: Chapter in Book/Report/Conference proceedingConference Abstract/Poster in proceedingAcademicpeer-review

Abstract

Construction and analysis of distributed systems is difficult; choreographic programming is a deadlock-freedom-by-construction approach to simplify it. In this paper, we present a new theory of choreographic programming. It supports for the first time: construction of distributed systems that require decentralised decision making (i.e., if/while-statements with multiparty conditions); analysis of distributed systems to provide not only deadlock freedom but also functional correctness (i.e., pre/postcondition reasoning). Both contributions are enabled by a single new technique, namely a predicate transformer for choreographies.

Original languageEnglish
Title of host publicationProgramming Languages and Systems
Subtitle of host publication31st European Symposium on Programming, ESOP 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2–7, 2022, Proceedings
Editors Ilya Sergey
PublisherSpringer
Pages520-547
Volume13240
Edition1
ISBN (Electronic)978-3-030-99336-8
ISBN (Print)978-3-030-99335-1
DOIs
Publication statusPublished - 2022
Event1st European Symposium on Programming and the European Joint Conferences on Theory and Practice of Software - Munich, Germany
Duration: 2 Apr 20227 Apr 2022

Publication series

SeriesLecture Notes in Computer Science
Volume13240
ISSN0302-9743

Conference

Conference1st European Symposium on Programming and the European Joint Conferences on Theory and Practice of Software
Abbreviated titleESOP 2022 and ETAPS 2022
Country/TerritoryGermany
CityMunich
Period2/04/227/04/22

Fingerprint

Dive into the research topics of 'A Predicate Transformer for Choreographies - Computing Preconditions in Choreographic Programming.'. Together they form a unique fingerprint.

Cite this