[Club2] Mi. 12.04; 14.00 Uhr !!! John von Neumann!!!

[Norbert Schirmer]

Diese Woche:

Mi. 12.04.06; 14.00 Uhr im John von Neumann (00.11.038)

Stefan Berghofer:

Title: A solution to the PoplMark challenge in Isabelle/HOL

Abstract:

We present a solution to the PoplMark challenge designed by Pierce et al.,
which has as a goal the formalization of the meta-theory of System Fsub.
The formalization is carried out in the theorem prover Isabelle/HOL using an
encoding based on de Bruijn indices. We start with a relatively simple 
formalization covering only the basic features of System Fsub, and explain 
how it can be extended later on to also cover records and more advanced 
binding constructs.

   Norbert