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

lmcs:1642 - Logical Methods in Computer Science, June 29, 2016, Volume 12, Issue 2 - https://doi.org/10.2168/LMCS-12(2:10)2016
Using higher-order contracts to model session typesArticle

Authors: Giovanni Bernardi ; Matthew Hennessy

    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
    Funding:
      Source : OpenAIRE Graph
    • Lero - the Irish Software Research Centre; Code: 13/RC/2094

    25 Documents citing this article

    Consultation statistics

    This page has been seen 1369 times.
    This article's PDF has been downloaded 446 times.