ICE-TCS Lectures Series - Luca Aceto - A Rule Format for Unit Elements

The next ICE-TCS  talk for this semester will be delivered on Friday, 30 October, by Luca Aceto (Reykjavik University). The talk, entitled A Rule Format for Unit Elements, will be held in room K5 at Reykjavík University (Kringlan 1) from 14:00 till 15:00.  The abstract for the seminar is appended.

Further information about forthcoming ICE- TCS events may be found at the news page

We look forward to seeing you at ICE- TCS events.

Abstract

In this talk, I will discuss a generic rule format for Structural Operational Semantics in the style of Plotkin guaranteeing that certain basic programs act as left- or right-unit elements for a set of binary operators.  I will show the generality of the format by applying it to a wide range of operators from the literature on process calculi, which are prototype languages for the description of parallel processes.

Results like the one I will present serve multiple purposes. Firstly, they pave the way for a tool-set that can mechanically prove semantic properties via syntactic means without involving user interaction. Secondly, they provide us with an insight as to the semantic nature of basic algebraic properties and its link to the syntax of the rules defining the operational semantics of languages. In other words, our rule formats may serve as a guideline for language designers who want to ensure, a priori, that the constructs under design enjoy certain basic algebraic properties.

This is joint work with Anna Ingolfsdottir (RU), MohammadReza Mousavi (TU Eindhoven) and Michel Reniers (TU Eindhoven) that will appear in the Proceedings of "SOFSEM 2010: The 36th International Conference on Current Trends in Theory and Practice of Computing", Lecture Notes in Computer Science, Springer-Verlag, 2010.