ﻻ يوجد ملخص باللغة العربية
We present Cho-Reo-graphies (CR), a new language model that unites two powerful programming paradigms for concurrent software based on communicating processes: Choreographic Programming and Exogenous Coordination. In CR, programmers specify the desired communications among processes using a choreography, and define how communications should be concretely animated by connectors given as constraint automata (e.g., synchronous barriers and asynchronous multi-casts). CR is the first choreography calculus where different communication semantics (determined by connectors) can be freely mixed; since connectors are user-defined, CR also supports many communication semantics that were previously unavailable for choreographies. We develop a static analysis that guarantees that a choreography in CR and its user-defined connectors are compatible, define a compiler from choreographies to a process calculus based on connectors, and prove that compatibility guarantees deadlock-freedom of the compiled process implementations.
Choreographic Programming is a correct-by-construction paradigm where a compilation procedure synthesises deadlock-free, concurrent, and distributed communicating processes from global, declarative descriptions of communications, called choreographie
We present Choral, the first language for programming choreographies (multiparty protocols) that builds on top of mainstream programming abstractions: in Choral, choreographies are objects. Given a choreography that defines interactions among some ro
We present Multiparty Classical Choreographies (MCC), a language model where global descriptions of communicating systems (choreographies) implement typed multiparty sessions. Typing is achieved by generalising classical linear logic to judgements th
Modular programming is a cornerstone in software development, as it allows to build complex systems from the assembly of simpler components, and support reusability and substitution principles. In a distributed setting, component assembly is supporte
Reo is an interaction-centric model of concurrency for compositional specification of communication and coordination protocols. Formal verification tools exist to ensure correctness and compliance of protocols specified in Reo, which can readily be (