2026-07-29T18:02:14Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:18200 2024-03-06T11:01:21Z ddc:004 open_access

Modular Compilation for Higher-Order Functional Choreographies Cruz-Filipe, Luís Graversen, Eva Lugović, Lovro Montesi, Fabrizio Peressotti, Marco Choreographies Concurrency λ-calculus Type Systems Choreographic programming is a paradigm for concurrent and distributed software, whereby descriptions of the intended communications (choreographies) are automatically compiled into distributed code with strong safety and liveness properties (e.g., deadlock-freedom). Recent efforts tried to combine the theories of choreographic programming and higher-order functional programming, in order to integrate the benefits of the former with the modularity of the latter. However, they do not offer a satisfactory theory of compilation compared to the literature, because of important syntactic and semantic shortcomings: compilation is not modular (editing a part might require recompiling everything) and the generated code can perform unexpected global synchronisations. In this paper, we find that these shortcomings are not mere coincidences. Rather, they stem from genuine new challenges posed by the integration of choreographies and functions: knowing which participants are involved in a choreography becomes nontrivial, and divergence in applications requires rethinking how to prove the semantic correctness of compilation. We present a novel theory of compilation for functional choreographies that overcomes these challenges, based on types and a careful design of the semantics of choreographies and distributed code. The result: a modular notion of compilation, which produces code that is deadlock-free and correct (it operationally corresponds to its source choreography). Schloss Dagstuhl – Leibniz-Zentrum für Informatik Luís Cruz-Filipe and Eva Graversen and Lovro Lugović and Fabrizio Montesi and Marco Peressotti 2023 Is Part Of LIPIcs, Volume 263, 37th European Conference on Object-Oriented Programming (ECOOP 2023) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.ECOOP.2023.7 urn:nbn:de:0030-drops-182005 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2023.7 eng https://creativecommons.org/licenses/by/4.0/legalcode