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.

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

Submitted 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

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.

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, Lecture notes in computer science, The Different Shades of Infinite Session Types, pp. 347-367, 2022, 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, Lecture notes in computer science, Session Coalgebras: A Coalgebraic View on Session Types and Communication Protocols, pp. 375-403, 2021, 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.

Luca Ciccone;Luca Padovani, International Colloquium on Automata, Languages and Programming, Inference Systems with Corules for Fair Subtyping and Liveness Properties of Binary Session Types, 198, pp. 1-16, 2021, 10.4230/lipics.icalp.2021.125.

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, Institutional Research Information System University of Turin (University of Turin), Two notions of sub-behaviour for session-based client/server systems: 10 Years Later, pp. 1-3, 2020, Bologna Italy, 10.1145/3414080.3414082, http://hdl.handle.net/2318/1759630.

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

Omar Inverso;Hernán C. Melgratti;Luca Padovani;Catia Trubiani;Emilio Tuosto, International Conference on Concurrency Theory, Probabilistic Analysis of Binary Sessions, 171, pp. 21-, 2020, 10.4230/lipics.concur.2020.14.

Simon J. Gay;Peter Thiemann;Vasco T. Vasconcelos, 2020, Duality of Session Types: The Final Cut, arXiv (Cornell University), 314, pp. 23-33, 10.4204/eptcs.314.3.

Vasco T. Vasconcelos;Filipe Casal;Bernardo Almeida;Andreia Mordido, Lecture notes in computer science, Mixed Sessions, pp. 715-742, 2020, 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, Lecture notes in computer science, From Behavioural Contracts to Session Types, pp. 278-297, 2019, 10.1007/978-3-030-21485-2_16.

Giuseppe Castagna;Mariangiola Dezani-Ciancaglini;Elena Giachino;Luca Padovani, Institutional Research Information System University of Turin (University of Turin), Foundations of Session Types, 13, pp. 1-3, 2019, Porto Portugal, 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, Science of Computer Programming, 167, pp. 25-50, 10.1016/j.scico.2018.06.005, https://doi.org/10.1016/j.scico.2018.06.005.

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, https://doi.org/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, https://doi.org/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, https://doi.org/10.1016/j.jlamp.2018.12.002.

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

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

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

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

Sources : OpenCitations, OpenAlex & Crossref

Share and export

Consultation statistics

This page has been seen 1991 times.

This article's PDF has been downloaded 537 times.