Towards Refinable Choreographies
Copyright policy )Towards Refinable Choreographies
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.
In Proceedings ICE 2020, arXiv:2009.07628
- University of Buenos Aires Argentina
- University of Turin Italy
- Gran Sasso Science Institute Italy
- Universidid De Buenos Aires Argentina
- National Institute for Nuclear Physics Italy
FOS: Computer and information sciences, Computer Science - Logic in Computer Science, choreography, Type Inference, Choreography; Refinement; Typing, Computer Science - Software Engineering, Artificial Intelligence, Logic Programming and Knowledge Representation, Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.), Computer Science - Logic in Computer Science; Computer Science - Logic in Computer Science; Computer Science - Software Engineering; D.1.3; D.2.4; D.3.1; F.3.1, refinement, D.1.3; D.2.4; D.3.1; F.3.1, D.1.3, D.3.1, typing, D.2.4, Computer science, Logic in Computer Science (cs.LO), Software Engineering (cs.SE), Computational Theory and Mathematics, Computer Science, Physical Sciences, F.3.1, Program Analysis and Verification Techniques, Formal Methods in Software Verification and Control
FOS: Computer and information sciences, Computer Science - Logic in Computer Science, choreography, Type Inference, Choreography; Refinement; Typing, Computer Science - Software Engineering, Artificial Intelligence, Logic Programming and Knowledge Representation, Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.), Computer Science - Logic in Computer Science; Computer Science - Logic in Computer Science; Computer Science - Software Engineering; D.1.3; D.2.4; D.3.1; F.3.1, refinement, D.1.3; D.2.4; D.3.1; F.3.1, D.1.3, D.3.1, typing, D.2.4, Computer science, Logic in Computer Science (cs.LO), Software Engineering (cs.SE), Computational Theory and Mathematics, Computer Science, Physical Sciences, F.3.1, Program Analysis and Verification Techniques, Formal Methods in Software Verification and Control
selected citations These citations are derived from selected sources.This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).2 popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network.Average influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).Average impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network.Average
Citations provided by BIP!Popularity provided by BIP!