[isabelle] AFP 2014 released / new entries

The Archive of Formal proofs is now available for Isabelle2014 at http://afp.sf.net.

The following development entries are now available as release versions from the
front page:

Skew Heap
Tobias Nipkow

Skew heaps are an amazingly simple and lightweight implementation of priority
queues. They were invented by Sleator and Tarjan [SIAM 1986] and have
logarithmic amortized complexity. This entry provides executable and verified
functional skew heaps. The amortized complexity of skew heaps is analyzed in the
AFP entry Amortized Complexity.
Splay Tree
Tobias Nipkow

Splay trees are self-adjusting binary search trees which were invented by
Sleator and Tarjan [JACM 1985]. This entry provides executable and verified
functional splay trees. The amortized complexity of splay trees is analyzed in
the AFP entry Amortized Complexity.
Amortized Complexity Verified
Tobias Nipkow

A framework for the analysis of the amortized complexity of (functional) data
structures is formalized in Isabelle/HOL and applied to a number of standard
examples and to two non-trivial ones: skew heaps and splay trees. In the same
spirit we show that the move-to-front algorithm for the list update problem is

A preliminary paper describing this research has been presented at the Isabelle
Workshop 2014.
Haskell's Show-Class in Isabelle/HOL
Christian Sternagel and René Thiemann

We implemented a type-class for pretty-printing, similar to Haskell's
Show-class. Moreover, we provide instantiations for Isabelle/HOL’s standard
types like bool, prod, sum, nats, ints, and rats. It is further possible, to
automatically derive pretty-printer for arbitrary user defined datatypes similar
to Haskell's "deriving Show".
Formal Specification of a Generic Separation Kernel
Freek Verbeek, Sergey Tverdyshev, Oto Havle, Holger Blasum, Bruno Langenstein,
Werner Stephan, Yakoub Nemouchi, Abderrahmane Feliachi, Burkhart Wolff and
Julien Schmaltz

Intransitive noninterference has been a widely studied topic in the last few
decades. Several well-established methodologies apply interactive theorem
proving to formulate a noninterference theorem over abstract academic models. In
joint work with several industrial and academic partners throughout Europe, we
are helping in the certification process of PikeOS, an industrial separation
kernel developed at SYSGO. In this process, established theories could not be
applied. We present a new generic model of separation kernels and a new theory
of intransitive noninterference. The model is rich in detail, making it suitable
for formal verification of realistic and industrial systems such as PikeOS.
Using a refinement-based theorem proving approach, we ensure that proofs remain

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.