ICE-TCS Lectures Series - Arnar Birgisson - Rule Formats for Determinism and Idempotency
On Friday, February 20th, Arnar Birgisson (Reykjavik University) delivers an ICE-TCS seminar. The talk is entitled Rule Formats for Determinism and Idempotency and will be held at 2pm in room K-5 at Reykjavik University (Kringlan 1).
ABSTRACT
Structural Operational Semantics (SOS) is a popular method for assigning a rigorous meaning to specification and programming languages. The meta-theory of SOS provides powerful tools for proving semantic properties for such languages without investing too much time on the actual proofs; it offers syntactic templates for SOS rules, called rule formats, which guarantee semantic properties once the SOS rules conform to the templates. In this talk, I will discuss rule formats for two (related) properties, namely, determinism and idempotence.
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. I will show the applicability of our formats by applying them to various operational semantics from the literature.
This talk is based on joint work with Luca Aceto (RU), Anna Ingolfsdottir (RU), MohammadReza Mousavi (TU Eindhoven) and Michel Reniers (TU Eindhoven), which will be presented at FSEN 2009, the third International Conference on Fundamentals of Software Engineering.
