[Club2] 12.03; 14:00 (Turing)

[Norbert Schirmer]

Am Montag, 12.03, ab 14:00 im Turing (00.09.055):

Florian Haftmann:

We present a code generator framework for Isabelle/HOL.  It formalizes
the intermediate stages between the purely logical description in terms
of equational theorems and a programming language.  Correctness of the
translation is established by giving the intermediate languages (a
subset of Haskell) an equational semantics and relating it back to the
logical level.  To allow code generation for SML, we present a prove
correct a (dictionary-based) translation eliminating type classes.  The
design of our framework covers different functional target languages.


This talk is meant to provide a high-level overview on a paper to be
submitted for TPHOL.  It is recommended to have a printout at hand
(~haftmann/world/codegen.pdf).  Feedback highly wellcome.


    Norbert