*To*: <isabelle-users at cl.cam.ac.uk>*Subject*: [isabelle] announcing AFP 2016-1*From*: <Gerwin.Klein at data61.csiro.au>*Date*: Sun, 18 Dec 2016 02:30:02 +0000*Accept-language*: en-AU, en-US*Thread-index*: AQHSWNaioSjOoxjd5k2KQ7tyKlajcw==*Thread-topic*: announcing AFP 2016-1

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

**Follow-Ups**:**Re: [isabelle] announcing AFP 2016-1***From:*Lars Hupel

- Previous by Date: Re: [isabelle] Haskabelle and Literate Haskell
- Next by Date: Re: [isabelle] using Haskabelle with recent versions of GHC
- Previous by Thread: Re: [isabelle] using Haskabelle with recent versions of GHC
- Next by Thread: Re: [isabelle] announcing AFP 2016-1
- Cl-isabelle-users December 2016 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list