[Club2] Quickie! HEUTE: 15:00

Norbert Schirmer schirmer@in.tum.de
Wed, 29 Mar 2006 10:49:34 +0200


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