[Club2] Fr. 22.09; 11.30 (Turing)

[Norbert Schirmer]

Diese Woche:

Freitag, 22.09.2006; 11:30: Raum Alan Turing: 00.09.055

  Amine Chaieb

  "Reflection for the masses"

   Abstract

Reflecting a type t, typically formulae or arithmetical terms, in the logic 
consists of defining a datatype r and a function 
interp:: [a1,.., an, r] --> t that maps any element of r into an element of t, 
und the possible use of the context encoded by a1 ... an. The process of 
transforming a term x::t back into to its r-corresponding form: interp y1 .. 
yn s, is called reification. In our talk we show how to automate reification 
for a useful class of interpretations. This work has been successfully 
implemented in Isabelle/HOL.


   Norbert