Towards Refinable Choreographies
Ugo de'Liguoro (Universit\`a di Torino), Hern\'an Melgratti, (Universidad de Buenos Aires), Emilio Tuosto (Gran Sasso Science Institute)
TL;DR
This paper explores the concept of refinable global choreographies, proposing a typing discipline to ensure well-formedness and analyzing how refinements affect protocol implementability.
Contribution
It introduces refinable choreographies with a typing discipline to maintain well-formedness and formalizes their relation to admissible refinements.
Findings
Refinable choreographies allow underspecified protocols that can be refined into actual protocols.
The typing discipline guarantees well-formedness of choreographies.
A formal relation among refinable choreographies and their refinements is established.
Abstract
We investigate refinement in the context of choreographies. We introduce refinable global choreographies allowing for the underspecification of protocols, whose interactions can be refined into actual protocols. Arbitrary refinements may spoil well-formedness, that is the sufficient conditions that guarantee a protocol to be implementable. We introduce a typing discipline that enforces well-formedness of typed choreographies. Then we unveil the relation among refinable choregraphies and their admissible refinements in terms of an axiom scheme.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.