Choreographies, logically

DOI10.1007/S00446-017-0295-1MaRDI QIDQ1699421zbMATH OpenOpenAlexFDO

Authors Marco Carbone, Fabrizio Montesi, Carsten Schürmann

Publication date 23 February 2018

Published in Distributed Computing (Search for Journal in Brave)

Full work available at URL https://portal.findresearcher.sdu.dk/da/publications/ccd494a0-74af-4b09-989b-9de5e268c89e

zbMATH Keywords

programming languageschoreographieslinear logicCurry-Howard isomorphism

Mathematics Subject Classification ID

Proof-theoretic aspects of linear logic and other substructural logics (03F52) Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

• Choreographies, logically
• Applied Choreographies
• Compositional choreographies
• The Paths to Choreography Extraction
• A core model for choreographic programming

Cites work

• Compositional choreographies
• Conversation Types
• Deadlock-freedom-by-design, multiparty asynchronous global programming
• Deciding choreography realizability
• From communicating machines to graphical choreographies
• Global Progress in Dynamically Interleaved Multiparty Sessions
• Higher-order processes, functions, and sessions: a monadic integration
• Hypersequents, logical consequence and intermediate logics for concurrency
• Linear logic
• Linear logical relations for session-based concurrency
• On the \(\pi\)-calculus and linear logic
• Procedural Choreographic Programming
• Propositions as sessions
• Session types as intuitionistic linear propositions
• Structured Communication-Centred Programming for Web Services
• Synthesising Choreographies from Local Session Types
• The Paths to Choreography Extraction
• The \(\pi\)-calculus: A theory of mobile processes
• \(\pi\)-calculus, internal mobility, and agent-passing calculi

Cited in

(19)

• From communicating machines to graphical choreographies
• Connecting open systems of communicating finite state machines
• A predicate transformer for choreographies. Computing preconditions in choreographic programming
• Compositional choreographies
• Certifying choreography compilation
• An abstract semantics of the global view of choreographies
• Choreographies, logically
• On the concurrent computational content of intermediate logics
• Guess Who’s Coming: Runtime Inclusion of Participants in Choreographies
• Applied Choreographies
• Realisability of choreographies
• Multiparty classical choreographies
• From infinity to choreographies. Extraction for unbounded systems
• Certified compilation of choreographies with \textsf{hacc}
• Data-driven choreographies à la Klaim
• From global choreographies to verifiable efficient distributed implementations
• Deciding choreography realizability
• Taking linear logic apart
• scientific article; zbMATH DE number 790829 (Why is no real title available?)

This page was built for publication: Choreographies, logically

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1699421)