[isabelle] AFP 2011 released

AFP 2011 has now been released. This means all entries available from the front page [http://afp.sf.net] now work by default with Isabelle2011.

The AFP now has 88 entries, in total encompassing over 500,000 lines of formal proof development.

The release makes the following two entries available from the front page that were previously accessible as development versions only.

Functional Binomial Queues
by René Neumann


Priority queues are an important data structure and efficient implementations of them are crucial. We implement a functional variant of binomial queues in Isabelle/HOL and show its functional correctness. A verification against an abstract reference specification of priority queues has also been attempted, but could not be achieved to the full extent.

Lower Semincontinous Functions
by Bogdan Grechuk


We define the notions of lower and upper semicontinuity for functions from a metric space to the extended real line. We prove that a function is both lower and upper semicontinuous if and only if it is continuous. We also give several equivalent characterizations of lower semicontinuity. In particular, we prove that a function is lower semicontinuous if and only if its epigraph is a closed set. Also, we introduce the notion of the lower semicontinuous hull of an arbitrary function and prove its basic properties.


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