Extending dynamic logic for reasoning about evolving algebras

The aim of this paper is to provide a logic for reasoning about
evolving algebras. This is done by extending a variant of dynamic
logic with additional program constructs: update of functions,
extension of universes, and simultaneous execution. A calculus for
this extended dynamic logic can be obtained from a sequent calculus
for (not extended) dynamic logic only by adding further rules, but
without modifications of original rules. This gives us reason to hope
that the KIV system (Karlsruhe Interactive Verifier) can be turned
into a tool for reasoning about evolving algebras only by extending
it, i.e. without (substantially) modifying existing code.