ACG

Combining Bialgebraic Semantics and Equations

It was observed by Turi and Plotkin that structural operational semantics can be studied at the level of universal coalgebra, providing specification formats for well-behaved operations at a general level. We extend this framework with non-structural assignment rules which can express, for example, the syntactic format for structural congruences proposed by Mousavi and Reniers. Our main result is that the operational model of such an extended specification is well-behaved, in the sense that bisimilarity is a congruence and that bisimulation-up-to techniques are sound.

Other presentations

On the specification of operations on the rational behaviour of systems

Published: di 30 oktober 2012
By Jurriaan Rot

In presentations.

Abstract: Structural operational semantics can be studied at the general level of distributive laws of syntax over behaviour. This yields speciﬁcation formats for well-behaved algebraic operations on final coalgebras, which are a domain for the behaviour of all systems of a given type functor. We introduce a format for …
read more
Model checking a language with unbounded object creation

Published: di 25 mei 2010
By Jurriaan Rot

In presentations.

We introduce a block-structured programming language which supports object creation, global variables, static scope and recursive procedures with local variables. Because of the combination of recursion, local variables and object creation, the behavior of the program is determined by infinitely many different states. However, we show that a program can …
read more

Page 1 / 1

Other presentations

hosted by

social