A Predicate Transformer for Choreographies: Computing Preconditions in Choreographic Programming

Sung-Shik Jongmans; Petra van den Bos

doi:10.1007/978-3-030-99336-8_19

A Predicate Transformer for Choreographies: Computing Preconditions in Choreographic Programming

Sung-Shik Jongmans^*
, Petra van den Bos

^*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

15 Citations (Scopus)

132 Downloads (Pure)

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 language	English
Title of host publication	Programming Languages and Systems
Subtitle of host publication	31st 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
Place of Publication	Cham
Publisher	Springer
Pages	520-547
Number of pages	28
ISBN (Print)	978-3-030-99336-8
DOIs	https://doi.org/10.1007/978-3-030-99336-8_19
Publication status	Published - 29 Mar 2022
Event	31st European Symposium on Programming, ESOP 2022 - Munich, Germany Duration: 2 Apr 2022 → 7 Apr 2022 Conference number: 31

Conference

Conference	31st European Symposium on Programming, ESOP 2022
Abbreviated title	ESOP 2022
Country/Territory	Germany
City	Munich
Period	2/04/22 → 7/04/22
Other	Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022

Access to Document

10.1007/978-3-030-99336-8_19Licence: CC BY

978-3-030-99336-8_19Final published version, 667 KBLicence: CC BY

Cite this

Jongmans, S.-S., & van den Bos, P. (2022). A Predicate Transformer for Choreographies: Computing Preconditions in Choreographic Programming. In I. Sergey (Ed.), Programming Languages and Systems: 31st 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 (pp. 520-547). Springer. https://doi.org/10.1007/978-3-030-99336-8_19

Jongmans, Sung-Shik ; van den Bos, Petra. / A Predicate Transformer for Choreographies : Computing Preconditions in Choreographic Programming. Programming Languages and Systems: 31st 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. editor / Ilya Sergey. Cham : Springer, 2022. pp. 520-547

@inproceedings{6e5270423c31496689d1f470e6fe55e3,

title = "A Predicate Transformer for Choreographies: Computing Preconditions in Choreographic Programming",

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.",

author = "Sung-Shik Jongmans and \{van den Bos\}, Petra",

year = "2022",

month = mar,

day = "29",

doi = "10.1007/978-3-030-99336-8\_19",

language = "English",

isbn = "978-3-030-99336-8",

pages = "520--547",

editor = "Ilya Sergey",

booktitle = "Programming Languages and Systems",

publisher = "Springer",

address = "Germany",

note = "31st European Symposium on Programming, ESOP 2022, ESOP 2022 ; Conference date: 02-04-2022 Through 07-04-2022",

}

Jongmans, S-S & van den Bos, P 2022, A Predicate Transformer for Choreographies: Computing Preconditions in Choreographic Programming. in I Sergey (ed.), Programming Languages and Systems: 31st 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. Springer, Cham, pp. 520-547, 31st European Symposium on Programming, ESOP 2022, Munich, Germany, 2/04/22. https://doi.org/10.1007/978-3-030-99336-8_19

A Predicate Transformer for Choreographies: Computing Preconditions in Choreographic Programming. / Jongmans, Sung-Shik; van den Bos, Petra.
Programming Languages and Systems: 31st 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. ed. / Ilya Sergey. Cham: Springer, 2022. p. 520-547.

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - A Predicate Transformer for Choreographies

T2 - 31st European Symposium on Programming, ESOP 2022

AU - Jongmans, Sung-Shik

AU - van den Bos, Petra

N1 - Conference code: 31

PY - 2022/3/29

Y1 - 2022/3/29

N2 - 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.

AB - 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.

U2 - 10.1007/978-3-030-99336-8_19

DO - 10.1007/978-3-030-99336-8_19

M3 - Conference contribution

SN - 978-3-030-99336-8

SP - 520

EP - 547

BT - Programming Languages and Systems

A2 - Sergey, Ilya

PB - Springer

CY - Cham

Y2 - 2 April 2022 through 7 April 2022

ER -

Jongmans SS, van den Bos P. A Predicate Transformer for Choreographies: Computing Preconditions in Choreographic Programming. In Sergey I, editor, Programming Languages and Systems: 31st 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. Cham: Springer. 2022. p. 520-547 doi: 10.1007/978-3-030-99336-8_19

A Predicate Transformer for Choreographies: Computing Preconditions in Choreographic Programming

Abstract

Conference

Access to Document

Fingerprint

Cite this