An algebra of behavioural types (Q418153): Difference between revisions
From MaRDI portal
Created a new Item |
ReferenceBot (talk | contribs) Changed an Item |
||
(7 intermediate revisions by 6 users not shown) | |||
Property / author | |||
Property / author: Vasco Thudichum Vasconcelos / rank | |||
Property / author | |||
Property / author: Vasco Thudichum Vasconcelos / rank | |||
Normal rank | |||
Property / review text | |||
The paper is concerned with type systems for concurrent objects. Typically, a type system is a set of axioms and inference rules which act as an abstract proof system aimed at guaranteeing, for example, that a function is always called with the right number of arguments. In the case of concurrent objects, static typing with interfaces-as-types is not sufficient when it comes to dealing with dynamic changes of the interface (the set of currently enabled methods). To address this problem, the paper introduces the simple algebra of behavioural types (ABT), inspired by CCS-like process algebraic models. ADT terms are meant to characterise life cycles of concurrent objects. As the corresponding states represent changing interfaces, such terms describe sequences of methods being offered, and can be used for typing concurrent objects as well as reasoning about their behavioural correctness. The development of ADT induces in a natural way a novel notion of behavioural equivalence which is investigated in depth. In particular, the paper proposes its axiomatisation which is shown to be sound for general terms, and also complete in the case of a sublanguage of sequential image-finite expressions. | |||
Property / review text: The paper is concerned with type systems for concurrent objects. Typically, a type system is a set of axioms and inference rules which act as an abstract proof system aimed at guaranteeing, for example, that a function is always called with the right number of arguments. In the case of concurrent objects, static typing with interfaces-as-types is not sufficient when it comes to dealing with dynamic changes of the interface (the set of currently enabled methods). To address this problem, the paper introduces the simple algebra of behavioural types (ABT), inspired by CCS-like process algebraic models. ADT terms are meant to characterise life cycles of concurrent objects. As the corresponding states represent changing interfaces, such terms describe sequences of methods being offered, and can be used for typing concurrent objects as well as reasoning about their behavioural correctness. The development of ADT induces in a natural way a novel notion of behavioural equivalence which is investigated in depth. In particular, the paper proposes its axiomatisation which is shown to be sound for general terms, and also complete in the case of a sublanguage of sequential image-finite expressions. / rank | |||
Normal rank | |||
Property / reviewed by | |||
Property / reviewed by: Maciej Koutny / rank | |||
Normal rank | |||
Property / Mathematics Subject Classification ID | |||
Property / Mathematics Subject Classification ID: 68Q85 / rank | |||
Normal rank | |||
Property / Mathematics Subject Classification ID | |||
Property / Mathematics Subject Classification ID: 68Q60 / rank | |||
Normal rank | |||
Property / Mathematics Subject Classification ID | |||
Property / Mathematics Subject Classification ID: 68Q55 / rank | |||
Normal rank | |||
Property / Mathematics Subject Classification ID | |||
Property / Mathematics Subject Classification ID: 68N30 / rank | |||
Normal rank | |||
Property / zbMATH DE Number | |||
Property / zbMATH DE Number: 6038300 / rank | |||
Normal rank | |||
Property / zbMATH Keywords | |||
process algebra | |||
Property / zbMATH Keywords: process algebra / rank | |||
Normal rank | |||
Property / zbMATH Keywords | |||
type system | |||
Property / zbMATH Keywords: type system / rank | |||
Normal rank | |||
Property / zbMATH Keywords | |||
concurrent object | |||
Property / zbMATH Keywords: concurrent object / rank | |||
Normal rank | |||
Property / zbMATH Keywords | |||
behavioural equivalence | |||
Property / zbMATH Keywords: behavioural equivalence / rank | |||
Normal rank | |||
Property / zbMATH Keywords | |||
axiomatisation | |||
Property / zbMATH Keywords: axiomatisation / rank | |||
Normal rank | |||
Property / zbMATH Keywords | |||
soundness | |||
Property / zbMATH Keywords: soundness / rank | |||
Normal rank | |||
Property / zbMATH Keywords | |||
completeness | |||
Property / zbMATH Keywords: completeness / rank | |||
Normal rank | |||
Property / describes a project that uses | |||
Property / describes a project that uses: PIPER / rank | |||
Normal rank | |||
Property / MaRDI profile type | |||
Property / MaRDI profile type: MaRDI publication profile / rank | |||
Normal rank | |||
Property / full work available at URL | |||
Property / full work available at URL: https://doi.org/10.1016/j.ic.2011.12.005 / rank | |||
Normal rank | |||
Property / OpenAlex ID | |||
Property / OpenAlex ID: W1990799174 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Spatial and behavioral types in the pi-calculus / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: On the consistency of Koomen's fair abstraction rule / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: The lambda calculus, its syntax and semantics / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Algebra of communicating processes with abstraction / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: CONCUR '93. 4th international conference on concurrency theory, Hildesheim, Germany, August 23--26, 1993. Proceedings / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q4370350 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: The \(\pi\)-calculus in direct style / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q4355677 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Logical Semantics of Types for Concurrency / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Conversation types / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Types as models / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q3142557 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Bisimulation equivalence is decidable for all context-free processes / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Formal methods for open object-based distributed systems. FMOODS, IFIP TC6/ WG6. 1 3rd international conference, Florence, Italy, February 15--18, 1999 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q4255591 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Algebraic laws for nondeterminism and concurrency / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q4346206 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q4222868 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: A generic type system for the pi-calculus / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q4536437 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q4536623 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Results on the propositional \(\mu\)-calculus / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q2852014 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Process rewrite systems. / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q3992568 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: A complete axiomatisation for observational congruence of finite-state behaviours / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: A calculus of mobile processes. II / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Infinite results / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q4018066 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q4942014 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q4251124 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q4222938 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q5691098 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q2778806 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q3837262 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Strong types for coordinating active objects / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: State inference for dynamically changing interfaces / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q4329009 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q4778708 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q4536621 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: An algebra of behavioural types / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Bisimilarity of open terms. / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: An interpretation of typed objects into typed \(\pi\)-calculus / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q4941915 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: The type and effect discipline / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: A shorter proof to uniqueness of solutions of equations / rank | |||
Normal rank | |||
links / mardi / name | links / mardi / name | ||
Latest revision as of 07:13, 5 July 2024
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | An algebra of behavioural types |
scientific article |
Statements
An algebra of behavioural types (English)
0 references
24 May 2012
0 references
The paper is concerned with type systems for concurrent objects. Typically, a type system is a set of axioms and inference rules which act as an abstract proof system aimed at guaranteeing, for example, that a function is always called with the right number of arguments. In the case of concurrent objects, static typing with interfaces-as-types is not sufficient when it comes to dealing with dynamic changes of the interface (the set of currently enabled methods). To address this problem, the paper introduces the simple algebra of behavioural types (ABT), inspired by CCS-like process algebraic models. ADT terms are meant to characterise life cycles of concurrent objects. As the corresponding states represent changing interfaces, such terms describe sequences of methods being offered, and can be used for typing concurrent objects as well as reasoning about their behavioural correctness. The development of ADT induces in a natural way a novel notion of behavioural equivalence which is investigated in depth. In particular, the paper proposes its axiomatisation which is shown to be sound for general terms, and also complete in the case of a sublanguage of sequential image-finite expressions.
0 references
process algebra
0 references
type system
0 references
concurrent object
0 references
behavioural equivalence
0 references
axiomatisation
0 references
soundness
0 references
completeness
0 references
0 references