Selected Papers of the 23rd International Conference on Coordination Models and Languages (COORDINATION 2021)

Editors: Ferruccio Damiani, Ornela Dardha

1. Relating Functional and Imperative Session Types

Hannes Saffrich ; Peter Thiemann.
Imperative session types provide an imperative interface to session-typedcommunication. In such an interface, channel references are first-class objectswith operations that change the typestate of the channel. Compared tofunctional session type APIs, the program structure is simpler at the surface,but typestate is required to model the current state of communicationthroughout. Following an early work that explored the imperative approach, asignificant body of work on session types has neglected the imperative approachand opts for a functional approach that uses linear types to manage channelreferences soundly. We demonstrate that the functional approach subsumes theearly work on imperative session types by exhibiting a typing and semanticspreserving translation into a system of linear functional session types. Wefurther show that the untyped backwards translation from the functional to theimperative calculus is semantics preserving. We restrict the type system of thefunctional calculus such that the backwards translation becomes typepreserving. Thus, we precisely capture the difference in expressiveness of thetwo calculi and conclude that the lack of expressiveness in the imperativecalculus is largely due to restrictions imposed by its type system.

2. A theory of Automated Market Makers in DeFi

Massimo Bartoletti ; James Hsin-yu Chiang ; Alberto Lluch-Lafuente.
Automated market makers (AMMs) are one of the most prominent decentralizedfinance (DeFi) applications. AMMs allow users to trade different types ofcrypto-tokens, without the need to find a counter-party. There are severalimplementations and models for AMMs, featuring a variety of sophisticatedeconomic mechanisms. We present a theory of AMMs. The core of our theory is anabstract operational model of the interactions between users and AMMs, whichcan be concretised by instantiating the economic mechanisms. We exploit ourtheory to formally prove a set of fundamental properties of AMMs,characterizing both structural and economic aspects. We do this by abstractingfrom the actual economic mechanisms used in implementations, and identifyingsufficient conditions which ensure the relevant properties. Notably, we devisea general solution to the arbitrage problem, the main game-theoretic foundationbehind the economic mechanisms of AMMs.

3. Deconfined Global Types for Asynchronous Sessions

Francesco Dagnino ; Paola Giannini ; Mariangiola Dezani-Ciancaglini.
Multiparty sessions with asynchronous communications and global types play animportant role for the modelling of interaction protocols in distributedsystems. In designing such calculi the aim is to enforce, by typing, goodproperties for all participants, maximising, at the same time, the acceptedbehaviours. Our type system improves the state-of-the-art by typing allasynchronous sessions and preserving the key properties of Subject Reduction,Session Fidelity and Progress when some well-formedness conditions aresatisfied. The type system comes together with a sound and complete typeinference algorithm. The well-formedness conditions are undecidable, but analgorithm checking an expressive restriction of them recovers the effectivenessof typing.

4. Concurrent Process Histories and Resource Transducers

Chad Nester.
We identify the algebraic structure of the material histories generated byconcurrent processes. Specifically, we extend existing categorical theories ofresource convertibility to capture concurrent interaction. Our formalism admitsan intuitive graphical presentation via string diagrams for proarrowequipments. We also consider certain induced categories of resourcetransducers, which are of independent interest due to their unusual structure.