We propose Klaim as a suitable base for a novel choreographic framework. More precisely we advocate Klaim as a suitable language onto which to project data-driven global specifications based on distributed tuple spaces. These specifications, akin to behavioural types, describe the coordination from a global point of view. Differently from behavioural types though, our specifications express the data flow across distributed tuple spaces rather than detailing the communication pattern of processes. We devise a typing system to validate Klaim programs against projections of our global specifications. An interesting feature of our typing approach is that well-typed systems have an arbitrary number of participants. In standard approaches based on behavioural types, this is often achieved at the cost of considerable technical complications.
Roberto Bruni, Andrea Corradini, Fabio Gadducci, Ugo Montanari, Emilio Tuosto, Hernán Melgratti, Springer