Rule Formats for Determinism and Idempotence
- Speaker
Luca Aceto (ICE-TCS, School of Computer Science, Reykjavik University, Iceland)
- Date and Time
Monday, May 31st 2010, at 10:15
- Location
Polacksbacken, room 1145
- 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 talk, I will discuss two (related) meta-theorems for guaranteeing determinism and idempotence of binary operators. These meta-theorems are formulated in terms of syntactic templates for operational semantics, called rule formats. I will argue for the applicability of the proposed formats by applying them to various operational semantics from the literature.
The talk is based on joint work with Arnar Birgisson (Chalmers), Anna Ingolfsdottir (Reykjavik University), MohammadReza Mousavi (TU Eindhoven) and Michel A. Reniers (TU Eindhoven). An extended abstract of the work is in the Proceedings of FSEN 2009 and a journal version will appear in Science of Computer Programming.