[Club2] 3 Club2 talks this week, on Wednesday starting at 2 PM

[Andrei Popescu]

Dear All, 
This Wednesday we have 3 diploma thesis talks. Details below.
Cheers,   Andrei 
Fabian ImmlerPicard Lindeloef and Numerical Analysis in Isabelle/HOL=======================================================Wed. Nov. 2, 14:00, MI 00.09.055 ("Alan Turing")
This work gives formalisations of initial value problems and provesthe existence of a unique solution (known as the Picard-Lindeloeftheorem) in Isabelle/HOL. Moreover, one-step methods for a numericalapproximation of the solution are analysed. We give executablespecifications for several Runge-Kutta methods and prove an
 explicitbound for the global error of the Euler method. 

Marcel RuegenbergSemi-automatic proof refactoring for Isabelle====================================================Wed. Nov. 2, 14:30, MI 00.09.055 ("Alan Turing")
Refactorings are semantics-preserving code transformations that are usually aimed at improving the structure or readability of source code. A standard example is the renaming of a value. In many integrated development environments for programming languages, automated support for refactoring is a standard feature.In contrast, refactoring in proof assistants such as Isabelle is, to date, a mostly manual and correspondingly tedious and
 error-prone process.This talk describes the motivation behind, and the implementation and capabilities of a tool, Levity, for proof refactoring in Isabelle that was developed in the course of a recent bachelor's thesis.

Michael Kerscher  Visualisation of Mira testdata====================================================Wed. Nov. 2, 15:00, MI 00.09.055 ("Alan Turing")
The presentation briefly introduces the development model of Isabelleand what Mira does. After presenting the currently used methods andtheir weaknesses of analysing the
 performance of Isabelle a newvisualisation tool is demonstrated.
I will explain how this tool works, how its individual parts communicatewith each other and what problems had to be solved during the creationof this new tool. As CouchDB and Mercurial are involved in the project,the necessary concepts are briefly explained during the talk.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/club2/attachments/20111031/88984a0f/attachment.html>