DC FieldValueLanguage
dc.contributor.authorGhilezan, Silviaen
dc.contributor.authorJakšić, Svetlanaen
dc.contributor.authorPantović, Jovankaen
dc.contributor.authorScalas, Alcesteen
dc.contributor.authorYoshida, Nobukoen
dc.date.accessioned2020-05-02T16:42:18Z-
dc.date.available2020-05-02T16:42:18Z-
dc.date.issued2019-04-01en
dc.identifier.issn2352-2208-
dc.identifier.urihttp://researchrepository.mi.sanu.ac.rs/handle/123456789/2575-
dc.description.abstractThis paper proves the soundness and completeness, together referred to as preciseness, of the subtyping relation for a synchronous multiparty session calculus. We address preciseness from operational and denotational viewpoints. The operational preciseness has been recently developed with respect to type safety, i.e., the safe replacement of a process of a smaller type in a context where a process of a bigger type is expected. The denotational preciseness is based on the denotation of a type: a mathematical object describing the meaning of the type, in accordance with the denotations of other expressions from the language. The main technical contribution of this paper is a novel proof strategy for the operational completeness of subtyping. We develop the notion of characteristic global type of a session type T, which describes a deadlock-free circular communication protocol involving all participants appearing in T. We prove operational completeness by showing that, if we place a process not conforming to a subtype of T in a context that matches the characteristic global type of T, then we obtain a deadlock. The denotational preciseness is proved as a corollary of the operational preciseness.en
dc.publisherElsevier-
dc.relationEPSRC EP/K011715/1, EP/K034413/1, EP/L00058X/1, EP/N027833/1 and EP/N028201/1-
dc.relationRepresentations of logical structures and formal languages and their application in computing-
dc.relationDevelopment of new information and communication technologies, based on advanced mathematical methods, with applications in medicine, telecommunications, power systems, protection of national heritage and education-
dc.relationCOST Action EUTYPES (CA15123), BETTY (IC1201) and ARVI (IC1402)-
dc.relationContinuous Observation of Embedded Multicore Systems-
dc.relation.ispartofJournal of Logical and Algebraic Methods in Programmingen
dc.subjectConcurrency | Multiparty session types | Process calculi | Subtypingen
dc.titlePrecise subtyping for synchronous multiparty sessionsen
dc.typeArticleen
dc.identifier.doi10.1016/j.jlamp.2018.12.002en
dc.identifier.scopus2-s2.0-85069436653en
dc.relation.firstpage127en
dc.relation.lastpage173en
dc.relation.volume104en
dc.description.rankM21-
item.grantfulltextnone-
item.cerifentitytypePublications-
item.openairecristypehttp://purl.org/coar/resource_type/c_18cf-
item.openairetypeArticle-
item.fulltextNo Fulltext-
crisitem.author.orcid0000-0003-2253-8285-
crisitem.project.projectURLhttp://www.mi.sanu.ac.rs/novi_sajt/research/projects/174026e.php-
crisitem.project.projectURLhttp://www.mi.sanu.ac.rs/novi_sajt/research/projects/044006e.php-
crisitem.project.fundingProgramDirectorate for Social, Behavioral & Economic Sciences-
crisitem.project.fundingProgramNATIONAL HEART, LUNG, AND BLOOD INSTITUTE-
crisitem.project.openAireinfo:eu-repo/grantAgreement/NSF/Directorate for Social, Behavioral & Economic Sciences/1740267-
crisitem.project.openAireinfo:eu-repo/grantAgreement/NIH/NATIONAL HEART, LUNG, AND BLOOD INSTITUTE/5R01HL044006-04-
Show simple item record

SCOPUSTM   
Citations

25
checked on Mar 28, 2024

Page view(s)

66
checked on Mar 29, 2024

Google ScholarTM

Check

Altmetric

Altmetric


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.