[Club2] ITP rehearsals

[Johannes Hölzl]

Dear Club2,

The coming Wednesday, Aug 8., the presenters at the ITP and the Isabelle
Workshop will rehearse their presentations.

As usual Club2 is in Alan Turing (MI 00.09.055) and it starts at 2 pm.

Best regards,
  Johannes


Abstract Interpretation of Annotated Commands
Tobias Nipkow
====================================================

This paper formalizes a generic abstract interpreter for a while-language,
including widening and narrowing. The collecting seman- tics and the abstract
interpreter operate on annotated commands: the program is represented as a
syntax tree with the semantic information directly embedded, without auxiliary
labels. The aim of the paper is sim- plicity of the formalization, not
efficiency or precision. This is motivated by the inclusion of the material in a
theorem prover based course on semantics.

--

Proof Pearl: A Probabilistic Proof for the Girth-Chromatic Number Theorem
Lars Noschinski
====================================================

The probabilistic method is a powerful tool for existence proofs in 
discrete mathematics. We formalize a probabilistic proof for the 
well-known theorem Girth-Chromatic Number theorem to explore how 
feasible such proofs are in a modern theorem prover.

--

Numerical Analysis of Ordinary Differential Equations in Isabelle/HOL
Fabian Immler and Johannes Hölzl
====================================================

Since many ordinary differential equations (ODEs) do not have a
closed solution, approximating them is an important problem in
numerical analysis. This work formalizes a method to approximate
solutions of ODEs in Isabelle/HOL.

We formalize initial value problems (IVPs) of ODEs and prove the
existence of a unique solution, i.e. the Picard-Lindelöf
theorem. We introduce general one-step methods for numerical
approximation of the solution and provide an analysis regarding the
local and global error of one-step methods.

We give an executable specification of the Euler method to
approximate the solution of IVPs. With user-supplied proofs for
bounds of the differential equation we can prove an explicit bound
for the global error. We use arbitrary-precision floating-point
numbers and also handle rounding errors when we truncate the numbers
for efficiency reasons.

--

Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL
Brian Huffman and Ondřej Kunčar
====================================================

Quotients, subtypes, and other forms of type abstraction are ubiquitous
in formal reasoning with higher-order logic. Typically, users want to build
a library of operations and theorems about an abstract type, but they
want to write definitions and proofs in terms of a more concrete
representation type, or “raw” type. Earlier work on the Isabelle Quotient
package has yielded great progress in automation, but it still has many
technical limitations. We present an improved, modular design centered
around two new packages: the Transfer package for proving theorems,
and the Lifting package for defining constants. Our new design is
simpler, applicable in more situations, and has more user-friendly
automation.

An initial implementation is available in Isabelle 2012.