Euler IMI

The seminar
"Computer methods in Proof Assistance"

St. Petersburg, Russia
June 2, 2009

The seminar is organized by Saint Petersburg Department of Steklov Institute of Mathematics RAS and IRIT (Toulouse, France) in the frame of collaboration program between Saint Petersburg Department of Steklov Institute of Mathematics RAS and IRIT (Toulouse, France) during the visit of prof. Sergey Soloviev to Saint Petersburg Department of Steklov Institute of Mathematics and Euler International Institute (May 30 - June 5).

Organizers:

Nikolay Vassiliev (PDMI RAS, St.Petersburg)
Sergey Soloviev (IRIT, Toulouse, France)

Agenda:

1. L. Feraud, M. Rebout, S. Soloviev. L. Marie-Magdeleine

The double pushout pullback approach to graph transformations.
There exist several approaches to attributed graph rewriting (generalization of word rewriting) based on category theory. One of best known is called a "double pushout" approach. One of drawbacks of this approach is that computations with attributes (using algebraic data types) are separated from categorical constructions used in graph rewriting part. We propose a unified approach where attributes are represented by inductive types and a "dual" construction of pullback is used to represent computations with attributes. In the end of the talk we discuss applications to models and metamodels in software engineering and possibilities of eneralization to infinite graphs and models.
(The talk presented by S. Soloviev)

2. S. Soloviev also presented an outline of the following work by J.-P. Bahsoun et al.

An Arbitrary Tree-Structured Replica Control Protocol (describing a method of optimized manipulations of multiple replicas (copies) of data)

Registered participants:

Nikolay Vasiliev (PDMI)
Sergey Soloviev (IRIT)
Fedor Novikov (IPA RAS)
Dmitry Pavlov (SPbGTU)
Michail Rybalkin(SPbGTU)
Sergey Baranov (Motorola)
Alexander Flegontov (St.Petersburg Pedagogical University)
Oleg Prosorov (PDMI)
Valeriya Nikolaenko (SPbGTU)