Publikation: On Hierarchical Communication Topologies in the π-calculus
Lade...
Dateien
Zu diesem Dokument gibt es keine Dateien.
Datum
2016
Autor:innen
Ong, C.-H. Luke
Herausgeber:innen
ISSN der Zeitschrift
Electronic ISSN
ISBN
Bibliografische Daten
Verlag
Schriftenreihe
Auflagebezeichnung
DOI (zitierfähiger Link)
Internationale Patentnummer
Angaben zur Forschungsförderung
Projekt
Open Access-Veröffentlichung
Core Facility der Universität Konstanz
Titel in einer weiteren Sprache
Publikationstyp
Beitrag zu einem Konferenzband
Publikationsstatus
Published
Erschienen in
THIEMANN, Peter, Hrsg.. Programming Languages and Systems : 25th European Symposium on Programming, ESOP 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Proceedings. Berlin: Springer, 2016, S. 149-175. Lecture Notes in Computer Science (LNCS). 9632. ISSN 0302-9743. eISSN 1611-3349. ISBN 978-3-662-49497-4. Verfügbar unter: doi: 10.1007/978-3-662-49498-1_7
Zusammenfassung
This paper is concerned with the shape invariants satisfied by the communication topology of π-terms, and the automatic inference of these invariants. A π-term P is hierarchical if there is a finite forest T such that the communication topology of every term reachable from P satisfies a T -shaped invariant. We design a static analysis to prove a term hierarchical by means of a novel type system that enjoys decidable inference. The soundness proof of the type system employs a non-standard view of π-calculus reactions. The coverability problem for hierarchical terms is decidable. This is proved by showing that every hierarchical term is depth-bounded, an undecidable property known in the literature. We thus obtain an expressive static fragment of the π-calculus with decidable safety verification problems.
Zusammenfassung in einer weiteren Sprache
Fachgebiet (DDC)
004 Informatik
Schlagwörter
Normal Form, Type System, Base Type, Typing Rule, Type Inference
Konferenz
25th European Symposium on Programming, ESOP 2016, 3. Apr. 2016 - 7. Apr. 2016, Eindhoven, The Netherlands
Rezension
undefined / . - undefined, undefined
Zitieren
ISO 690
D'OSUALDO, Emanuele, C.-H. Luke ONG, 2016. On Hierarchical Communication Topologies in the π-calculus. 25th European Symposium on Programming, ESOP 2016. Eindhoven, The Netherlands, 3. Apr. 2016 - 7. Apr. 2016. In: THIEMANN, Peter, Hrsg.. Programming Languages and Systems : 25th European Symposium on Programming, ESOP 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Proceedings. Berlin: Springer, 2016, S. 149-175. Lecture Notes in Computer Science (LNCS). 9632. ISSN 0302-9743. eISSN 1611-3349. ISBN 978-3-662-49497-4. Verfügbar unter: doi: 10.1007/978-3-662-49498-1_7BibTex
@inproceedings{DOsualdo2016Hiera-71004,
year={2016},
doi={10.1007/978-3-662-49498-1_7},
title={On Hierarchical Communication Topologies in the π-calculus},
number={9632},
isbn={978-3-662-49497-4},
issn={0302-9743},
publisher={Springer},
address={Berlin},
series={Lecture Notes in Computer Science (LNCS)},
booktitle={Programming Languages and Systems : 25th European Symposium on Programming, ESOP 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Proceedings},
pages={149--175},
editor={Thiemann, Peter},
author={D'Osualdo, Emanuele and Ong, C.-H. Luke}
}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/71004">
<dcterms:issued>2016</dcterms:issued>
<dc:language>eng</dc:language>
<dcterms:available rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2024-10-18T07:21:44Z</dcterms:available>
<dcterms:isPartOf rdf:resource="https://kops.uni-konstanz.de/server/rdf/resource/123456789/36"/>
<foaf:homepage rdf:resource="http://localhost:8080/"/>
<dspace:isPartOfCollection rdf:resource="https://kops.uni-konstanz.de/server/rdf/resource/123456789/36"/>
<dcterms:title>On Hierarchical Communication Topologies in the π-calculus</dcterms:title>
<dc:date rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2024-10-18T07:21:44Z</dc:date>
<dcterms:abstract>This paper is concerned with the shape invariants satisfied by the communication topology of π-terms, and the automatic inference of these invariants. A π-term P is hierarchical if there is a finite forest T such that the communication topology of every term reachable from P satisfies a T -shaped invariant. We design a static analysis to prove a term hierarchical by means of a novel type system that enjoys decidable inference. The soundness proof of the type system employs a non-standard view of π-calculus reactions. The coverability problem for hierarchical terms is decidable. This is proved by showing that every hierarchical term is depth-bounded, an undecidable property known in the literature. We thus obtain an expressive static fragment of the π-calculus with decidable safety verification problems.</dcterms:abstract>
<dc:creator>Ong, C.-H. Luke</dc:creator>
<dc:contributor>Ong, C.-H. Luke</dc:contributor>
<void:sparqlEndpoint rdf:resource="http://localhost/fuseki/dspace/sparql"/>
<bibo:uri rdf:resource="https://kops.uni-konstanz.de/handle/123456789/71004"/>
<dc:creator>D'Osualdo, Emanuele</dc:creator>
<dc:contributor>D'Osualdo, Emanuele</dc:contributor>
</rdf:Description>
</rdf:RDF>Interner Vermerk
xmlui.Submission.submit.DescribeStep.inputForms.label.kops_note_fromSubmitter
Prüfungsdatum der Dissertation
Finanzierungsart
Kommentar zur Publikation
Allianzlizenz
Corresponding Authors der Uni Konstanz vorhanden
Internationale Co-Autor:innen
Universitätsbibliographie
Nein
