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.


Source : oai:arXiv.org:1310.6176
DOI : 10.2168/LMCS-12(2:10)2016
Volume: Volume 12, Issue 2
Published on: June 29, 2016
Submitted on: August 11, 2016
Keywords: Computer Science - Logic in Computer Science


Share

Browsing statistics

This page has been seen 63 times.
This article's PDF has been downloaded 65 times.