| 1. |
- Aceto, Luca, et al.
(författare)
-
A Rule Format for Unit Elements
- 2009
-
Rapport (övrigt vetenskapligt/konstnärligt)abstract
- This paper offers a meta-theorem for languages with a Structural Operational Semantics (SOS) in the style of Plotkin. Namely, it proposes a generic rule format for SOS guaranteeing that certain constants act as left- or right-unit elements for a set of binary operators. We show the generality of our format by applying it to a wide range of operators from the literature on process calculi.
|
|
| 2. |
- Aceto, Luca, et al.
(författare)
-
A rule format for unit elements
- 2010
-
Ingår i: SOFSEM 2010. - Berlin : Springer Berlin/Heidelberg. - 9783642112652 - 9783642112669 ; , s. 141-152
-
Konferensbidrag (refereegranskat)abstract
- This paper offers a meta-theorem for languages with a Structural Operational Semantics (SOS) in the style of Plotkin. Namely, it proposes a generic rule format for SOS guaranteeing that certain constants act as left- or right-unit elements for a set of binary operators. We show the generality of our format by applying it to a wide range of operators from the literature on process calculi.
|
|
| 3. |
- Aceto, Luca, et al.
(författare)
-
Exploiting Algebraic Laws to Improve Mechanized Axiomatizations
- 2013
-
Ingår i: Algebra and Coalgebra in Computer Science. - Berlin : Springer Berlin/Heidelberg. - 9783642402067 - 9783642402050 ; , s. 36-50
-
Konferensbidrag (refereegranskat)abstract
- In the field of structural operational semantics (SOS), there have been several proposals both for syntactic rule formats guaranteeing the validity of algebraic laws, and for algorithms for automatically generating ground-complete axiomatizations. However, there has been no synergy between these two types of results. This paper takes the first steps in marrying these two areas of research in the meta-theory of SOS and shows that taking algebraic laws into account in the mechanical generation of axiomatizations results in simpler axiomatizations. The proposed theory is applied to a paradigmatic example from the literature, showing that, in this case, the generated axiomatization coincides with a classic hand-crafted one. © 2013 Springer-Verlag Berlin Heidelberg.
|
|
| 4. |
- Aceto, Luca, et al.
(författare)
-
Rule formats for determinism and idempotence
- 2012
-
Ingår i: Science of Computer Programming. - Amsterdam : Elsevier BV. - 0167-6423 .- 1872-7964. ; 77:7-8, s. 889-907
-
Tidskriftsartikel (refereegranskat)abstract
- Determinism is a semantic property of (a fragment of) a language that specifies that a program cannot evolve operationally in several different ways. Idempotence is a property of binary composition operators requiring that the composition of two identical specifications or programs will result in a piece of specification or program that is equivalent to the original components. In this paper, we propose (related) meta-theorems for guaranteeing the determinism and idempotence of binary operators. These meta-theorems are formulated in terms of syntactic templates for operational semantics, called rule formats. In order to obtain a powerful rule format for idempotence, we make use of the determinism of certain transition relations in the definition of the format for idempotence. We show the applicability of our formats by applying them to various operational semantics from the literature.
|
|
| 5. |
- Aceto, Luca, et al.
(författare)
-
Rule Formats for Distributivity
- 2012
-
Ingår i: Theoretical Computer Science. - : Elsevier BV. - 0304-3975 .- 1879-2294. ; 458, s. 1-28
-
Tidskriftsartikel (refereegranskat)abstract
- This paper proposes rule formats for Structural Operational Semantics guaranteeing that certain binary operators are left distributive with respect to a set of binary operators. Examples of left-distributivity laws from the literature are shown to be instances of the provided formats. Some conditions ensuring the invalidity of the left-distributivity law are also offered. © 2012 Elsevier B.V. All rights reserved.
|
|
| 6. |
- Aceto, Luca, et al.
(författare)
-
Rule Formats for Distributivity
- 2011
-
Ingår i: Language and Automata Theory and Applications. - Heidelberg : Springer Berlin/Heidelberg. - 9783642212536 ; , s. 79-90
-
Konferensbidrag (refereegranskat)abstract
- This paper proposes rule formats for Structural Operational Semantics guaranteeing that certain binary operators are left distributive with respect to a set of binary operators. Examples of left-distributivity laws from the literature are shown to be instances of the provided formats. © 2011 Springer-Verlag.
|
|
| 7. |
- Aceto, Luca, et al.
(författare)
-
SOS Rule Formats for Zero and Unit Elements
- 2011
-
Ingår i: Theoretical Computer Science. - Amsterdam : Elsevier. - 0304-3975 .- 1879-2294. ; 412:28, s. 3045-3071
-
Tidskriftsartikel (refereegranskat)abstract
- This paper proposes rule formats for Structural Operational Semantics guaranteeing that certain constants act as left or right unit/zero elements for a set of binary operators. Examples of left and right zero, as well as unit, elements from the literature are shown to fit the rule formats offered in this study. © 2011 Elsevier B.V. All rights reserved.
|
|
