Bernardi, Giovanni and Hennessy, Matthew - Using higher-order contracts to model session types

lmcs:1642 - Logical Methods in Computer Science, June 29, 2016, Volume 12, Issue 2 -
Using higher-order contracts to model session types

Authors: Bernardi, Giovanni and Hennessy, Matthew

Session types are used to describe and structure interactions between independent processes in distributed systems. Higher-order types are needed in order to properly structure delegation of responsibility between processes. In this paper we show that higher-order web-service contracts can be used to provide a fully-abstract model of recursive higher-order session types. The model is set-theoretic, in the sense that the meaning of a contract is given in terms of the set of contracts with which it complies. The proof of full-abstraction depends on a novel notion of the complement of a contract. This in turn gives rise to an alternative to the type duality commonly used in systems for type-checking session types. We believe that the notion of complement captures more faithfully the behavioural intuition underlying type duality.

Volume: Volume 12, Issue 2
Published on: June 29, 2016
Submitted on: May 23, 2015
Keywords: Computer Science - Logic in Computer Science


Consultation statistics

This page has been seen 361 times.
This article's PDF has been downloaded 197 times.