Email Gateway (Aug 22 2022 at 14:40): Email Gateway (Aug 22 2022 at 14:40):From: Lars Hupel <hupel@in.tum.de>
Dear (prospective) AFP authors,
the submission system has also been updated to work with Isabelle2016-1.
Also, we have implemented a couple of new features since initial launch
in March. Most notably, it is now possible to submit multiple entries at
once, and the submission system performs some additional checks on the
sources (e.g. use of prohibited commands).
As always: in case something doesn't work as expected, please feel free
to mail me (or the mailing list).
Cheers
Lars
Email Gateway (Aug 22 2022 at 14:54):From: Gerwin.Klein@data61.csiro.au
The Archive of Formal Proofs is now available for Isabelle2016-1 from http://isa-afp.org
As always, previous releases for previous Isabelle versions remain available, and there is a whole host of (ten) new entries available from the front page.
Our new statistics page is now also available for the release version. You can watch the archive growing and prospering at https://www.isa-afp.org/statistics.shtml
Enjoy!
Gerwin
Abstract Interpretation of Annotated Commands
by Tobias Nipkow
This is the Isabelle formalization of the material decribed in the eponymous ITP 2012 paper. It develops a generic abstract interpreter for a while-language, including widening and narrowing. The collecting semantics 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 formalization is simplicity, not efficiency or precision. This is motivated by the inclusion of the material in a theorem prover based course on semantics. A similar (but more polished) development is covered in the book Concrete Semantics.
https://www.isa-afp.org/entries/Abs_Int_ITP2012.shtml
The Factorization Algorithm of Berlekamp and Zassenhaus
by Jose Divasón, Sebastiaan Joosten, René Thiemann, and Akihisa Yamada
We formalize the Berlekamp-Zassenhaus algorithm for factoring square-free integer polynomials in Isabelle/HOL. We further adapt an existing formalization of Yun’s square-free factorization algorithm to integer polynomials, and thus provide an efficient and certified factorization algorithm for arbitrary univariate polynomials.
The algorithm first performs a factorization in the prime field GF(p) and then performs computations in the integer ring modulo p^k, where both p and k are determined at runtime. Since a natural modeling of these structures via dependent types is not possible in Isabelle/HOL, we formalize the whole algorithm using Isabelle’s recent addition of local type definitions.
Through experiments we verify that our algorithm factors polynomials of degree 100 within seconds.
https://www.isa-afp.org/entries/Berlekamp_Zassenhaus.shtml
Catalan Numbers
by Manuel Eberl
In this work, we define the Catalan numbers Cn and prove several equivalent definitions (including some closed-form formulae). We also show one of their applications (counting the number of binary trees of size n), prove the asymptotic growth approximation Cn ∼ 4n / (√π · n1.5), and provide reasonably efficient executable code to compute them.
The derivation of the closed-form formulae uses algebraic manipulations of the ordinary generating function of the Catalan numbers, and the asymptotic approximation is then done using generalised binomial coefficients and the Gamma function. Thanks to these highly non-elementary mathematical tools, the proofs are very short and simple.
https://www.isa-afp.org/entries/Catalan_Numbers.shtml
Fisher–Yates shuffle
by Manuel Eberl
This work defines and proves the correctness of the Fisher–Yates algorithm for shuffling – i.e. producing a random permutation – of a list. The algorithm proceeds by traversing the list and in each step swapping the current element with a random element from the remaining list.
https://www.isa-afp.org/entries/Fisher_Yates.shtml
Formalization of Knuth–Bendix Orders for Lambda-Free Higher-Order Terms
by Heiko Becker, Jasmin Christian Blanchette, Uwe Waldmann, and Daniel Wand
This Isabelle/HOL formalization defines Knuth–Bendix orders for higher-order terms without lambda-abstraction and proves many useful properties about them. The main order fully coincides with the standard transfinite KBO with subterm coefficients on first-order terms. It appears promising as the basis of a higher-order superposition calculus.
https://www.isa-afp.org/entries/Lambda_Free_KBOs.shtml
Formalization of Recursive Path Orders for Lambda-Free Higher-Order Terms
by Jasmin Christian Blanchette, Uwe Waldmann, and Daniel Wand
This Isabelle/HOL formalization defines recursive path orders (RPOs) for higher-order terms without lambda-abstraction and proves many useful properties about them. The main order fully coincides with the standard RPO on first-order terms also in the presence of currying, distinguishing it from previous work. An optimized variant is formalized as well. It appears promising as the basis of a higher-order superposition calculus.
https://www.isa-afp.org/entries/Lambda_Free_RPOs.shtml
Lp spaces
by Sebastien Gouezel
Lp is the space of functions whose p-th power is integrable. It is one of the most fundamental Banach spaces that is used in analysis and probability. We develop a framework for function spaces, and then implement the Lp spaces in this framework using the existing integration theory in Isabelle/HOL. Our development contains most fundamental properties of Lp spaces, notably the Hölder and Minkowski inequalities, completeness of Lp, duality, stability under almost sure convergence, multiplication of functions in Lp and Lq, stability under conditional expectation.
https://www.isa-afp.org/entries/Lp.shtml
Formalization of Nested Multisets, Hereditary Multisets, and Syntactic Ordinals
by Jasmin Christian Blanchette, Mathias Fleury, and Dmitriy Traytel
This Isabelle/HOL formalization introduces a nested multiset datatype and defines Dershowitz and Manna's nested multiset order. The order is proved well founded and linear. By removing one constructor, we transform the nested multisets into hereditary multisets. These are isomorphic to the syntactic ordinals—the ordinals can be recursively expressed in Cantor normal form. Addition, subtraction, multiplication, and linear orders are provided on this type.
https://www.isa-afp.org/entries/Nested_Multisets_Ordinals.shtml
Pairing Heap
by Hauke Brinkop and Tobias Nipkow
This library defines three different versions of pairing heaps: a functional version of the original design based on binary trees [Fredman et al. 1986], the version by Okasaki [1998] and a modified version of the latter that is free of structural invariants.
The amortized complexity of pairing heaps is analyzed in the AFP article Amortized Complexity.
https://www.isa-afp.org/entries/Pairing_Heap.shtml
Stirling's formula
by Manuel Eberl
This work contains a proof of Stirling's formula both for the factorial n! ∼ √2πn (n/e)n on natural numbers and the real Gamma function Γ(x) ∼ √2π/x (x/e)x. The proof is based on work by Graham Jameson.
https://www.isa-afp.org/entries/Stirling_Formula.shtml
Last updated: Apr 24 2024 at 20:16 UTC