An algebra of behavioural types (Q418153): Difference between revisions
From MaRDI portal
Created a new Item |
Changed an Item |
||
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 |
Revision as of 21:04, 29 June 2023
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