[Club2] Code Generation from Inductive Predicates in Isabelle/HOL

[Florian Haftmann]

Am Fr 17. April 2009 um 10:00 im Alan Turing (00.09.055 ) hält

	Lukas Bulwahn

im Rahmen seiner Diplomarbeit einen Vortrag

	Code Generation from Inductive Predicates in Isabelle/HOL

Diese Arbeit präsentiert eine Übersetzung von induktiven Prädikaten zu
Gleichungen, die ein funktionales Programm beschreiben.  Die Korrektheit
der Übersetzung wird dabei zur Laufzeit formal bewiesen.

	Florian

-- 

Home:
http://wwwbroy.in.tum.de/~haftmann

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 252 bytes
Desc: OpenPGP digital signature
URL: <https://mailmanbroy.informatik.tu-muenchen.de/mailman/private/club2/attachments/20090407/9473451e/attachment.pgp>