[Club2] Fr. 1.12; 11:30; im J.v. Neumann!!!

[Norbert Schirmer]

This Friday, 1.12, 11:30 in room John v. Neumann (00.11.038)

Florian Haftmann:

State monads in Isabelle/HOL -- a proposal

Monads are a well-established concept in the Haskell community to
express a concept of "computations" by separating the core of
"computations" from their "aspect" (total computations, partial
computations, non-deterministic computations, state-sensitive
computations, ...).  State-sensitive computations are a key concept for
introducing destructive values into Haskell while keeping referential
transparency.

Monads are represented as constructor classes.  This forbids their
direct translation into HOL whose type system has no notion of
constructor classes.  However, one instance of monads is still
representable -- by restricting to the prominent example of
state-sensitive computations, still some noteworthy benefits can be
gained, including nice do-syntax instead of complicated state-plumbing
code.  The same approach not only affects the manner how things can be
written down in HOL but in some cases allows direct generation of
destructive code for Haskell.


    Norbert