文章基本信息

标题：Using higher-order contracts to model session types
本地全文：下载
作者：Giovanni Bernardi ; Matthew Hennessy
期刊名称：Logical Methods in Computer Science
印刷版ISSN：1860-5974
电子版ISSN：1860-5974
出版年度：2016
卷号：12
期号：2
页码：1
DOI：10.2168/LMCS-12(2:10)2016
出版社：Technical University of Braunschweig
摘要：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.
其他关键词：recursive subtyping, higher-order types, duality, contract compliance, testing preorders