Email Gateway (Aug 18 2022 at 17:16): Email Gateway (Aug 18 2022 at 17:16):From: Gerwin Klein <gerwin.klein@nicta.com.au>
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
[http://afp.sf.net/entries/Binomial-Queues.shtml]
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
[http://afp.sf.net/entries/Lower_Semicontinuous.shtml]
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.
Cheers,
Gerwin
Last updated: Apr 24 2024 at 12:33 UTC