[Club2] (no subject)

[Andrei Popescu]

Dear All,  

In 10 minutes (at 14:00) we will have two talks: 

an IDP presentation by Sudeep Kanav (advised by Johannes) and a presentation by our
visitor Jose Divasón from Universidad de La Rioja (Spain).  
 
Cheers, 
  Andrei  


Formalization of Continuous Probability Distributions
Sudeep Kanav (IDP project with Johannes Hölzl)
======================================================================
Wed., Febr. 12, 14:00, Room: Turing (01.11.018)

We formalized important continuous probability distributions (Uniform, Exponential, 
Normal, and Erlang) in Isabelle/HOL. We defined them by
their probability density function (pdf) and characterized their cumulative
distribution function (cdf), expectation, variance and entropy as
closed form (as far as possible, c.f. normal distribution). Further, we show the
distribution of sums, products, minima and maxima of random variables with
certain distributions, e.g. the sum of two indep. normal distributed r.v. is
again normal distributed.


Formalisation and Execution of Linear Algebra algorithms using Isabelle/HOL
Jose Divasón
======================================================================
Wed., Febr. 12, 14:30, Room: Turing (01.11.018)

In this talk I am going to explain in broad terms my work up to now. It is mostly related to the formalisation of Linear Algebra algorithms, such as the Gauss-Jordan algorithm. This algorithm has been formalised in Isabelle and versions of it can be obtained in two different functional languages (SML and Haskell) by means of code generation techniques. Thanks to this formalisation, ranks, determinants, inverses, bases of the four fundamental subspaces of a matrix and solutions of a system of linear equations can be computed. The refinements and serialisations that have been carried out to improve the performance will be explained and also some applications of the work.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/club2/attachments/20140212/5166a04d/attachment.html>