[Club2] update on this Wednesday talks (Oct. 17, 16:00, Alonso Church)

[Andrei Popescu]

Dear All, 
This Wednesday, after the two already advertised talks we will also have Fabian Immler's master thesis talk. Details follow. 
Cheers,   Andrei 
Fabian Immler
Title: Generic Construction of Probability Spaces for Paths of
Stochastic Processes in Isabelle/HOL

Abstract: Stochastic processes are used in probability theory to
describe the evolution of random systems over time. The principal
mathematical problem is the construction of a probability space for
the paths of stochastic processes. The Daniell-Kolmogorov theorem
solves this problem: it shows how a family of finite-dimensional
distributions defines the distribution of the stochastic process. The
construction is generic, i.e., it works for discrete time as well as
for continuous time.
Starting from the existing formalizations of measure theory and
product probability spaces in Isabelle/HOL, we provide a formal proof
of the Daniell-Kolmogorov theorem in Isabelle/HOL. This requires us to
formalize concepts from topology, namely polish spaces and regularity
of measures on polish spaces.
These results can serve as a foundation to formalize for example
discrete-time or continuous-time Markov chains, Markov decision
processes, or physical phenomena like Brownian motion.



--- On Sun, 10/14/12, Andrei Popescu <uuomul at yahoo.com> wrote:

From: Andrei Popescu <uuomul at yahoo.com>
Subject: talks on Wednesday Oct. 17, 16:00, Alonso Church
To: "club2" <club2 at mailbroy.informatik.tu-muenchen.de>
Date: Sunday, October 14, 2012, 4:23 AM
Dear All, 
The coming week we have two talks by Lukas's students on a locale visualization graph and a testing tool for ML.  Please note the unusual location.
Best regards,    Andrei 
Wed. Oct. 17, 16:00, 01.09.014 ("Alonzo Church") 
Markus Kaiser: Isabelle's Graphview------------------------------------------------
Markus Kaiser worked on the visualization of complex locale dependency graphs.
Isabelle offers with locales a mechanism for modular and abstract theory and specification development. The dependencies are in large projects very complex.
Goal of this work was the implementation of a graphical
 user interface to visualize these dependencies.
The presentation of graphs can be configured by the user for simplified views, e.g. to show or hide specific nodes or to aggregate nodes. The implementation is developed in Scala.
Nicolai Schaffroth: A Specification-based Testing Tool for Isabelle's ML Environment (Bachelor thesis)-------------------------------------------------

When writing software, it is often difficult to ensure the result works as intended.
Therefore, testing is an important part of software development, allowing the programmer to check the correctness of his program.  Unit tests with a large number of random test cases are typically used to validate that all functions fulfill their
 specification for any input.
In this thesis, I adapt a specification-based testing tool for use in the theorem prover Isabelle's ML environment, while further extending it to automatically generate appropriate test data.
 

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/club2/attachments/20121015/9c4d8b1c/attachment.html>