Publikation: A bunch of sessions : a propositions-as-sessions interpretation of bunched implications in channel-based concurrency
Dateien
Datum
Autor:innen
Herausgeber:innen
ISSN der Zeitschrift
Electronic ISSN
ISBN
Bibliografische Daten
Verlag
Schriftenreihe
Auflagebezeichnung
URI (zitierfähiger Link)
DOI (zitierfähiger Link)
Internationale Patentnummer
Link zur Lizenz
Angaben zur Forschungsförderung
Projekt
Open Access-Veröffentlichung
Core Facility der Universität Konstanz
Titel in einer weiteren Sprache
Publikationstyp
Publikationsstatus
Erschienen in
Zusammenfassung
The emergence of propositions-as-sessions, a Curry-Howard correspondence between propositions of Linear Logic and session types for concurrent processes, has settled the logical foundations of message-passing concurrency. Central to this approach is the resource consumption paradigm heralded by Linear Logic. In this paper, we investigate a new point in the design space of session type systems for message-passing concurrent programs. We identify O’Hearn and Pym’s Logic of Bunched Implications (BI) as a fruitful basis for an interpretation of the logic as a concurrent programming language. This leads to a treatment of non-linear resources that is radically different from existing approaches based on Linear Logic. We introduce a new π-calculus with sessions, called πBI; its most salient feature is a construct called spawn, which expresses new forms of sharing that are induced by structural principles in BI. We illustrate the expressiveness of πBI and lay out its fundamental theory: type preservation, deadlock-freedom, and weak normalization results for well-typed processes; an operationally sound and complete typed encoding of an affine λ-calculus; and a non-interference result for access of resources.
Zusammenfassung in einer weiteren Sprache
Fachgebiet (DDC)
Schlagwörter
Konferenz
Rezension
Zitieren
ISO 690
FRUMIN, Dan, Emanuele D'OSUALDO, Bas VAN DEN HEUVEL, Jorge A. PÉREZ, 2022. A bunch of sessions : a propositions-as-sessions interpretation of bunched implications in channel-based concurrency. In: Proceedings of the ACM on Programming Languages. Association for Computing Machinery (ACM). 2022, 6(OOPSLA2), S. 841-869. eISSN 2475-1421. Verfügbar unter: doi: 10.1145/3563318BibTex
@article{Frumin2022-10-31bunch-71011, year={2022}, doi={10.1145/3563318}, title={A bunch of sessions : a propositions-as-sessions interpretation of bunched implications in channel-based concurrency}, number={OOPSLA2}, volume={6}, journal={Proceedings of the ACM on Programming Languages}, pages={841--869}, author={Frumin, Dan and D'Osualdo, Emanuele and van den Heuvel, Bas and Pérez, Jorge A.} }
RDF
<rdf:RDF xmlns:dcterms="http://purl.org/dc/terms/" xmlns:dc="http://purl.org/dc/elements/1.1/" xmlns:rdf="http://www.w3.org/1999/02/22-rdf-syntax-ns#" xmlns:bibo="http://purl.org/ontology/bibo/" xmlns:dspace="http://digital-repositories.org/ontologies/dspace/0.1.0#" xmlns:foaf="http://xmlns.com/foaf/0.1/" xmlns:void="http://rdfs.org/ns/void#" xmlns:xsd="http://www.w3.org/2001/XMLSchema#" > <rdf:Description rdf:about="https://kops.uni-konstanz.de/server/rdf/resource/123456789/71011"> <dcterms:rights rdf:resource="https://rightsstatements.org/page/InC/1.0/"/> <dcterms:issued>2022-10-31</dcterms:issued> <dc:rights>terms-of-use</dc:rights> <dc:creator>Pérez, Jorge A.</dc:creator> <dcterms:available rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2024-10-18T08:37:42Z</dcterms:available> <dc:creator>D'Osualdo, Emanuele</dc:creator> <bibo:uri rdf:resource="https://kops.uni-konstanz.de/handle/123456789/71011"/> <dcterms:isPartOf rdf:resource="https://kops.uni-konstanz.de/server/rdf/resource/123456789/36"/> <dcterms:title>A bunch of sessions : a propositions-as-sessions interpretation of bunched implications in channel-based concurrency</dcterms:title> <dc:contributor>D'Osualdo, Emanuele</dc:contributor> <dc:creator>van den Heuvel, Bas</dc:creator> <dc:contributor>Frumin, Dan</dc:contributor> <void:sparqlEndpoint rdf:resource="http://localhost/fuseki/dspace/sparql"/> <dc:contributor>Pérez, Jorge A.</dc:contributor> <foaf:homepage rdf:resource="http://localhost:8080/"/> <dspace:isPartOfCollection rdf:resource="https://kops.uni-konstanz.de/server/rdf/resource/123456789/36"/> <dcterms:abstract>The emergence of propositions-as-sessions, a Curry-Howard correspondence between propositions of Linear Logic and session types for concurrent processes, has settled the logical foundations of message-passing concurrency. Central to this approach is the resource consumption paradigm heralded by Linear Logic. In this paper, we investigate a new point in the design space of session type systems for message-passing concurrent programs. We identify O’Hearn and Pym’s Logic of Bunched Implications (BI) as a fruitful basis for an interpretation of the logic as a concurrent programming language. This leads to a treatment of non-linear resources that is radically different from existing approaches based on Linear Logic. We introduce a new π-calculus with sessions, called πBI; its most salient feature is a construct called spawn, which expresses new forms of sharing that are induced by structural principles in BI. We illustrate the expressiveness of πBI and lay out its fundamental theory: type preservation, deadlock-freedom, and weak normalization results for well-typed processes; an operationally sound and complete typed encoding of an affine λ-calculus; and a non-interference result for access of resources.</dcterms:abstract> <dc:contributor>van den Heuvel, Bas</dc:contributor> <dcterms:hasPart rdf:resource="https://kops.uni-konstanz.de/bitstream/123456789/71011/4/Frumin_2-177ny2adhlv9n6.pdf"/> <dc:date rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2024-10-18T08:37:42Z</dc:date> <dc:creator>Frumin, Dan</dc:creator> <dspace:hasBitstream rdf:resource="https://kops.uni-konstanz.de/bitstream/123456789/71011/4/Frumin_2-177ny2adhlv9n6.pdf"/> <dc:language>eng</dc:language> </rdf:Description> </rdf:RDF>