Using higher-order contracts to model session types
| Autor: | Bernardi, Giovanni, Hennessy, Matthew |
|---|---|
| Rok vydání: | 2013 |
| Předmět: | |
| Zdroj: | Logical Methods in Computer Science, Volume 12, Issue 2 (June 29, 2016) lmcs:1642 |
| Druh dokumentu: | Working Paper |
| DOI: | 10.2168/LMCS-12(2:10)2016 |
| Popis: | 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. Comment: Added definitions of m-closed terms, of 'dual', and a discussion to show the problems of the complement function |
| Databáze: | arXiv |
| Externí odkaz: |
|