Using higher-order contracts to model session types

Giovanni Bernardi; Matthew Hennessy

doi:10.2168/LMCS-12(2:10)2016

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.

Comment: Added definitions of m-closed terms, of 'dual', and a discussion to show the problems of the complement function

https://doi.org/10.2168/LMCS-12(2:10)2016

Source: arXiv.org:1310.6176

Volume: Volume 12, Issue 2

Published on: June 29, 2016

Imported on: May 23, 2015

Keywords: Computer Science - Logic in Computer Science

Licence: arXiv.org - Non-exclusive license to distribute

Funding:

Source : OpenAIRE Graph

Lero - the Irish Software Research Centre; Code: 13/RC/2094

Classifications

Mathematics Subject Classification 2020¹

Sources:

[1] zbMATH Open.

Bibliographic References

25 Documents citing this article

Nobuko Yoshida;Ping Hou, 2024, Less is More Revisited, Lecture notes in computer science, pp. 268-291, 10.1007/978-3-031-66673-5_14.

Alex C. Keizer;Henning Basold;Jorge A. Pérez, 2022, Session Coalgebras: A Coalgebraic View on Regular and Context-free Session Types, ACM Transactions on Programming Languages and Systems, 44, 3, pp. 1-45, 10.1145/3527633, https://doi.org/10.1145/3527633.

Bernardo Almeida;Andreia Mordido;Peter Thiemann;Vasco T. Vasconcelos, 2022, Polymorphic lambda calculus with context-free session types, Information and Computation, 289, pp. 104948, 10.1016/j.ic.2022.104948, https://doi.org/10.1016/j.ic.2022.104948.

Farzaneh Derakhshan;Frank Pfenning, 2022, Circular Proofs as Session-Typed Processes: A Local Validity Condition, Logical Methods in Computer Science, Volume 18, Issue 2, 10.4230/lipics.concur.2020.12, https://doi.org/10.46298/lmcs-18(2:8)2022.

Luca Ciccone;Luca Padovani, 2022, Fair termination of binary sessions, Proceedings of the ACM on Programming Languages, 6, POPL, pp. 1-30, 10.1145/3498666, https://doi.org/10.1145/3498666.

Simon J. Gay;Diogo Poças;Vasco T. Vasconcelos, 2022, The Different Shades of Infinite Session Types, Lecture notes in computer science, pp. 347-367, 10.1007/978-3-030-99253-8_18, https://doi.org/10.1007/978-3-030-99253-8_18.

Alex C. Keizer;Henning Basold;Jorge A. Pérez, 2021, Session Coalgebras: A Coalgebraic View on Session Types and Communication Protocols, Lecture notes in computer science, pp. 375-403, 10.1007/978-3-030-72019-3_14, https://doi.org/10.1007/978-3-030-72019-3_14.

Filipe Casal;Andreia Mordido;Vasco T. Vasconcelos, 2021, Mixed sessions, Theoretical Computer Science, 897, pp. 23-48, 10.1016/j.tcs.2021.08.005, https://doi.org/10.1016/j.tcs.2021.08.005.

Mauricio Cano;Hugo A. López;Jorge A. Pérez;Camilo Rueda, 2021, Session-based concurrency, declaratively, Acta Informatica, 59, 1, pp. 1-87, 10.1007/s00236-021-00395-w, https://doi.org/10.1007/s00236-021-00395-w.

Franco Barbanera;Ugo de'Liguoro, 2020, Two notions of sub-behaviour for session-based client/server systems: 10 Years Later, Institutional Research Information System University of Turin (University of Turin), pp. 1-3, 10.1145/3414080.3414082, https://dl.acm.org/doi/10.1145/3414080.3414082.

Oleg Kiselyov;Keigo Imai, 2020, Session Types Without Sophistry, Lecture notes in computer science, pp. 66-87, 10.1007/978-3-030-59025-3_5.

Simon J. Gay;Peter Thiemann;Vasco T. Vasconcelos, 2020, Duality of Session Types: The Final Cut, Electronic Proceedings in Theoretical Computer Science, 314, pp. 23-33, 10.4204/eptcs.314.3, https://doi.org/10.4204/eptcs.314.3.

Vasco T. Vasconcelos;Filipe Casal;Bernardo Almeida;Andreia Mordido, 2020, Mixed Sessions, Lecture notes in computer science, pp. 715-742, 10.1007/978-3-030-44914-8_26, https://doi.org/10.1007/978-3-030-44914-8_26.

Alceste Scalas;Nobuko Yoshida, 2019, Less is more: multiparty session types revisited, Proceedings of the ACM on Programming Languages, 3, POPL, pp. 1-29, 10.1145/3290343, https://doi.org/10.1145/3290343.

Alessandro Fantechi;Elie Najm;Jean-Bernard Stefani, 2019, From Behavioural Contracts to Session Types, Lecture notes in computer science, pp. 278-297, 10.1007/978-3-030-21485-2_16.

Giuseppe Castagna;Mariangiola Dezani-Ciancaglini;Elena Giachino;Luca Padovani, 2019, Foundations of Session Types, Institutional Research Information System University of Turin (University of Turin), 13, pp. 1-3, 10.1145/3354166.3356340, http://hdl.handle.net/2318/1712465.

Alceste Scalas;Nobuko Yoshida, 2018, Multiparty session types, beyond duality, Journal of Logical and Algebraic Methods in Programming, 97, pp. 55-84, 10.1016/j.jlamp.2018.01.001, https://doi.org/10.1016/j.jlamp.2018.01.001.

Franco Barbanera;Ivan Lanese;Ugo de'Liguoro, 2018, A theory of retractable and speculative contracts, 167, pp. 25-50, 10.1016/j.scico.2018.06.005, https://inria.hal.science/hal-01912858.

Franco Barbanera;Ugo de'Liguoro, 2018, Session types and subtyping for orchestrated interactions, Journal of Logical and Algebraic Methods in Programming, 102, pp. 103-137, 10.1016/j.jlamp.2018.10.001.

Giovanni Bernardi;Adrian Francalanza, 2018, Full-abstraction for client testing preorders, Science of Computer Programming, 168, pp. 94-117, 10.1016/j.scico.2018.08.004.

Silvia Ghilezan;Svetlana Jakšić;Jovanka Pantović;Alceste Scalas;Nobuko Yoshida, 2018, Precise subtyping for synchronous multiparty sessions, Journal of Logical and Algebraic Methods in Programming, 104, pp. 127-173, 10.1016/j.jlamp.2018.12.002.

Franco Barbanera;Ivan Lanese;Ugo de’Liguoro, 2017, Retractable and Speculative Contracts, pp. 119-137, 10.1007/978-3-319-59746-1_7, https://inria.hal.science/hal-01633262.

Giovanni Bernardi;Adrian Francalanza, 2017, Full-Abstraction for Must Testing Preorders, pp. 237-255, 10.1007/978-3-319-59746-1_13, https://hal.inria.fr/hal-01657337.

Peter Thiemann;Vasco T. Vasconcelos, 2016, Context-free session types, Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, pp. 462-475, 10.1145/2951913.2951926.

Peter Thiemann;Vasco T. Vasconcelos, 2016, Context-free session types, ACM SIGPLAN Notices, 51, 9, pp. 462-475, 10.1145/3022670.2951926.

Sources : OpenCitations, OpenAlex & Crossref

Share and export

Consultation statistics

This page has been seen 3368 times.

This article's PDF has been downloaded 745 times.