Heute: 15.00 Uhr im Turing (00.09.055)
Norbert Schirmer
Statespaces --- The Locale Way
Abstract:
Verification of imperative programs is all about reasoning about the
modifications of a program state. How should the state be represented in
Isabelle/HOL? Some common approaches are discussed and a new flavour based on
a distinctive feature of Isabelle, namely locales, is proposed.
Norbert