Archivi categoria:

Seminar: Towards type-safe sessions in Scala

Upcoming Seminar

Towards type-safe sessions in Scala

September 7, 15.00 (Aula F)
Palazzo delle Scienze - Cagliari

Alceste Scalas
Imperial College London

I will present my ongoing work on LChannels, a Scala library for type-safe session-based communication.  I will first give a brief introduction to the Scala language, and to Akka, an industrial-grade framework for distributed applications. I will explain how LChannels achieves type-safe local and distributed communication by exploiting two fundamental features of Scala and Akka: Promises/Futures, and actors.  I will show how a protocol expressed as a session type can be converted into an LChannels protocol, and demonstrate how communication errors are detected at compile time.

Seminar: Compliance and subtyping in timed session types

Upcoming Seminar

Compliance and subtyping in timed session types

September 7, 15.45 (Aula F)
Palazzo delle Scienze - Cagliari

Maurizio Murgia
Dipartimento di Matematica e Informatica, Università degli Studi di Cagliari

We propose an extension of binary session types, to formalise timed communication protocols between two participants at the endpoints of a session. We introduce a decidable compliance relation, which generalises to the timed setting the usual progress-based notion of compliance between untimed session types. We then show a sound and complete technique to decide when a timed session type admits a compliant one, and if so, to construct the least session type compliant with a given one, according to the subtyping preorder induced by compliance. Decidability of subtyping follows from these results. We exploit our theory to design and implement a message-oriented middleware, where distributed modules with compliant protocols can be dynamically composed, and their communications monitored, so to guarantee safe interactions.

Vicious circles in contracts and in logic

Upcoming paper (to appear in Science of Computer Programming)

M. Bartoletti, T. Cimoli, P. Di Giamberardino, and R. Zunino

Abstract. Contracts are formal promises on the future interactions of participants, which describe the causal dependencies among their actions. An inherent feature of contracts is that such dependencies may be circular: for instance, a buyer promises to pay for an item if the seller promises to ship it, and vice versa. We establish a bridge between two formal models for contracts, one based on games over event structures, and the other one on Propositional Contract Logic. In particular, we show that winning strategies in the game-theoretic model correspond to proofs in the logic.

Choreographies in the wild

Upcoming paper (to appear in Science of Computer Programming)

M. Bartoletti, J. Lange, A. Scalas and R. Zunino

Abstract. We investigate the use of choreographies in distributed scenarios where, as in the real world, mutually distrusting (and possibly dishonest) participants may be unfaithful to their expected behaviour. In our model, each participant advertises its promised behaviour as a contract. Participants may interact through multiparty sessions, created when their contracts allow to synthesise a choreography. We show that systems of honest participants (which always adhere to their contracts) enjoy progress and session fidelity.