diff --git a/metadata/entries/Affine_Arithmetic.toml b/metadata/entries/Affine_Arithmetic.toml --- a/metadata/entries/Affine_Arithmetic.toml +++ b/metadata/entries/Affine_Arithmetic.toml @@ -1,34 +1,32 @@ title = "Affine Arithmetic" date = 2014-02-07 topics = [ "Mathematics/Analysis", ] abstract = """ We give a formalization of affine forms as abstract representations of zonotopes. We provide affine operations as well as overapproximations of some non-affine operations like multiplication and division. Expressions involving those operations can automatically be turned into (executable) functions approximating the original expression in affine arithmetic.""" license = "bsd" note = "" [authors] [authors.immler] homepage = "immler_homepage" [contributors] [notify] immler = "immler_email" [history] -2015-01-31 = """ -added algorithm for zonotope/hyperplane intersection
-""" +2015-01-31 = "added algorithm for zonotope/hyperplane intersection
" 2017-09-20 = """ linear approximations for all symbols from the floatarith data type""" [extra] [related] diff --git a/metadata/entries/Algebraic_Numbers.toml b/metadata/entries/Algebraic_Numbers.toml --- a/metadata/entries/Algebraic_Numbers.toml +++ b/metadata/entries/Algebraic_Numbers.toml @@ -1,43 +1,41 @@ title = "Algebraic Numbers in Isabelle/HOL" date = 2015-12-22 topics = [ "Mathematics/Algebra", ] abstract = """ Based on existing libraries for matrices, factorization of rational polynomials, and Sturm's theorem, we formalized algebraic numbers in Isabelle/HOL. Our development serves as an implementation for real and complex numbers, and it admits to compute roots and completely factorize real and complex polynomials, provided that all coefficients are rational numbers. Moreover, we provide two implementations to display algebraic numbers, an injective and expensive one, or a faster but approximative version.

To this end, we mechanized several results on resultants, which also required us to prove that polynomials over a unique factorization domain form again a unique factorization domain.

""" license = "bsd" note = "" [authors] [authors.thiemann] email = "thiemann_email" [authors.yamada] email = "yamada_email" [authors.joosten] email = "joosten_email" [contributors] [contributors.eberl] homepage = "eberl_homepage" [notify] thiemann = "thiemann_email" yamada = "yamada_email1" joosten = "joosten_email" [history] -2016-01-29 = """ -Split off Polynomial Interpolation and Polynomial Factorization
-""" +2016-01-29 = "Split off Polynomial Interpolation and Polynomial Factorization
" 2017-04-16 = "Use certified Berlekamp-Zassenhaus factorization, use subresultant algorithm for computing resultants, improved bisection algorithm" [extra] [related] diff --git a/metadata/entries/Amortized_Complexity.toml b/metadata/entries/Amortized_Complexity.toml --- a/metadata/entries/Amortized_Complexity.toml +++ b/metadata/entries/Amortized_Complexity.toml @@ -1,41 +1,37 @@ title = "Amortized Complexity Verified" date = 2014-07-07 topics = [ "Computer science/Data structures", ] abstract = """ 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 the folowing non-trivial ones: skew heaps, splay trees, splay heaps and pairing heaps.

A preliminary version of this work (without pairing heaps) is described in a paper published in the proceedings of the conference on Interactive Theorem Proving ITP 2015. An extended version of this publication is available here.""" license = "bsd" note = "" [authors] [authors.nipkow] homepage = "nipkow_homepage" [contributors] [notify] nipkow = "nipkow_email" [history] -2015-03-17 = """ -Added pairing heaps by Hauke Brinkop.
-""" -2016-07-12 = """ -Moved splay heaps from here to Splay_Tree
-""" +2015-03-17 = "Added pairing heaps by Hauke Brinkop.
" +2016-07-12 = "Moved splay heaps from here to Splay_Tree
" 2016-07-14 = "Moved pairing heaps from here to the new Pairing_Heap" [extra] [related] diff --git a/metadata/entries/Applicative_Lifting.toml b/metadata/entries/Applicative_Lifting.toml --- a/metadata/entries/Applicative_Lifting.toml +++ b/metadata/entries/Applicative_Lifting.toml @@ -1,42 +1,40 @@ title = "Applicative Lifting" date = 2015-12-22 topics = [ "Computer science/Functional programming", ] abstract = """ Applicative functors augment computations with effects by lifting function application to types which model the effects. As the structure of the computation cannot depend on the effects, applicative expressions can be analysed statically. This allows us to lift universally quantified equations to the effectful types, as observed by Hinze. Thus, equational reasoning over effectful computations can be reduced to pure types.

This entry provides a package for registering applicative functors and two proof methods for lifting of equations over applicative functors. The first method normalises applicative expressions according to the laws of applicative functors. This way, equations whose two sides contain the same list of variables can be lifted to every applicative functor.

To lift larger classes of equations, the second method exploits a number of additional properties (e.g., commutativity of effects) provided the properties have been declared for the concrete applicative functor at hand upon registration.

We declare several types from the Isabelle library as applicative functors and illustrate the use of the methods with two examples: the lifting of the arithmetic type class hierarchy to streams and the verification of a relabelling function on binary trees. We also formalise and verify the normalisation algorithm used by the first proof method.

""" license = "bsd" note = "" [authors] [authors.lochbihler] homepage = "lochbihler_homepage" [authors.schneider] [contributors] [notify] lochbihler = "lochbihler_email1" [history] -2016-03-03 = """ -added formalisation of lifting with combinators
-""" +2016-03-03 = "added formalisation of lifting with combinators
" 2016-06-10 = """ implemented automatic derivation of lifted combinator reductions; support arbitrary lifted relations using relators; improved compatibility with locale interpretation (revision ec336f354f37)
""" [extra] [related] diff --git a/metadata/entries/Approximation_Algorithms.toml b/metadata/entries/Approximation_Algorithms.toml --- a/metadata/entries/Approximation_Algorithms.toml +++ b/metadata/entries/Approximation_Algorithms.toml @@ -1,42 +1,40 @@ title = "Verified Approximation Algorithms" date = 2020-01-16 topics = [ "Computer science/Algorithms/Approximation", ] abstract = """ We present the first formal verification of approximation algorithms for NP-complete optimization problems: vertex cover, set cover, independent set, center selection, load balancing, and bin packing. The proofs correct incompletenesses in existing proofs and improve the approximation ratio in one case. A detailed description of our work (excluding center selection) has been published in the proceedings of IJCAR 2020.""" license = "bsd" note = "" [authors] [authors.essmann] email = "essmann_email" [authors.nipkow] homepage = "nipkow_homepage" [authors.robillard] homepage = "robillard_homepage" [authors.sulejmani] [contributors] [notify] nipkow = "nipkow_email" [history] -2021-02-08 = """ -added theory Approx_SC_Hoare (Set Cover) by Robin Eßmann
-""" +2021-02-08 = "added theory Approx_SC_Hoare (Set Cover) by Robin Eßmann
" 2021-06-29 = "added theory Center_Selection by Ujkan Sulejmani" [extra] [related] diff --git a/metadata/entries/Architectural_Design_Patterns.toml b/metadata/entries/Architectural_Design_Patterns.toml --- a/metadata/entries/Architectural_Design_Patterns.toml +++ b/metadata/entries/Architectural_Design_Patterns.toml @@ -1,42 +1,40 @@ title = "A Theory of Architectural Design Patterns" date = 2018-03-01 topics = [ "Computer science/System description languages", ] abstract = """ The following document formalizes and verifies several architectural design patterns. Each pattern specification is formalized in terms of a locale where the locale assumptions correspond to the assumptions which a pattern poses on an architecture. Thus, pattern specifications may build on top of each other by interpreting the corresponding locale. A pattern is verified using the framework provided by the AFP entry Dynamic Architectures. Currently, the document consists of formalizations of 4 different patterns: the singleton, the publisher subscriber, the blackboard pattern, and the blockchain pattern. Thereby, the publisher component of the publisher subscriber pattern is modeled as an instance of the singleton pattern and the blackboard pattern is modeled as an instance of the publisher subscriber pattern. In general, this entry provides the first steps towards an overall theory of architectural design patterns.""" license = "bsd" note = "" [authors] [authors.marmsoler] homepage = "marmsoler_homepage" [contributors] [notify] marmsoler = "marmsoler_email" [history] -2018-05-25 = """ -changing the major assumption for blockchain architectures from alternative minings to relative mining frequencies (revision 5043c5c71685)
-""" +2018-05-25 = "changing the major assumption for blockchain architectures from alternative minings to relative mining frequencies (revision 5043c5c71685)
" 2019-04-08 = "adapting the terminology: honest instead of trusted, dishonest instead of untrusted (revision 7af3431a22ae)" [extra] [related] diff --git a/metadata/entries/Collections.toml b/metadata/entries/Collections.toml --- a/metadata/entries/Collections.toml +++ b/metadata/entries/Collections.toml @@ -1,49 +1,45 @@ title = "Collections Framework" date = 2009-11-25 topics = [ "Computer science/Data structures", ] abstract = "This development provides an efficient, extensible, machine checked collections framework. The library adopts the concepts of interface, implementation and generic algorithm from object-oriented programming and implements them in Isabelle/HOL. The framework features the use of data refinement techniques to refine an abstract specification (using high-level concepts like sets) to a more concrete implementation (using collection datastructures, like red-black-trees). The code-generator of Isabelle/HOL can be used to generate efficient code." license = "bsd" note = "" [authors] [authors.lammich] homepage = "lammich_homepage" [contributors] [contributors.lochbihler] homepage = "lochbihler_homepage" [contributors.tuerk] [notify] lammich = "lammich_email" [history] 2010-10-08 = """ New Interfaces: OrderedSet, OrderedMap, List. Fifo now implements list-interface: Function names changed: put/get --> enqueue/dequeue. New Implementations: ArrayList, ArrayHashMap, ArrayHashSet, TrieMap, TrieSet. Invariant-free datastructures: Invariant implicitely hidden in typedef. Record-interfaces: All operations of an interface encapsulated as record. Examples moved to examples subdirectory.
""" -2010-12-01 = """ -New Interfaces: Priority Queues, Annotated Lists. Implemented by finger trees, (skew) binomial queues.
-""" +2010-12-01 = "New Interfaces: Priority Queues, Annotated Lists. Implemented by finger trees, (skew) binomial queues.
" 2011-10-10 = """ SetSpec: Added operations: sng, isSng, bexists, size_abort, diff, filter, iterate_rule_insertP MapSpec: Added operations: sng, isSng, iterate_rule_insertP, bexists, size, size_abort, restrict, map_image_filter, map_value_image_filter Some maintenance changes
""" -2012-04-25 = """ -New iterator foundation by Tuerk. Various maintenance changes.
-""" +2012-04-25 = "New iterator foundation by Tuerk. Various maintenance changes.
" [extra] [related] diff --git a/metadata/entries/Containers.toml b/metadata/entries/Containers.toml --- a/metadata/entries/Containers.toml +++ b/metadata/entries/Containers.toml @@ -1,45 +1,41 @@ title = "Light-weight Containers" date = 2013-04-15 topics = [ "Computer science/Data structures", ] abstract = """ This development provides a framework for container types like sets and maps such that generated code implements these containers with different (efficient) data structures. Thanks to type classes and refinement during code generation, this light-weight approach can seamlessly replace Isabelle's default setup for code generation. Heuristics automatically pick one of the available data structures depending on the type of elements to be stored, but users can also choose on their own. The extensible design permits to add more implementations at any time.

To support arbitrary nesting of sets, we define a linear order on sets based on a linear order of the elements and provide efficient implementations. It even allows to compare complements with non-complements.""" license = "bsd" note = "" [authors] [authors.lochbihler] homepage = "lochbihler_homepage" [contributors] [contributors.thiemann] email = "thiemann_email" [notify] lochbihler = "lochbihler_email1" [history] -2013-07-11 = """ -add pretty printing for sets (revision 7f3f52c5f5fa)
-""" +2013-07-11 = "add pretty printing for sets (revision 7f3f52c5f5fa)
" 2013-09-20 = """ provide generators for canonical type class instantiations (revision 159f4401f4a8 by René Thiemann)
""" -2014-07-08 = """ -add support for going from partial functions to mappings (revision 7a6fc957e8ed)
-""" +2014-07-08 = "add support for going from partial functions to mappings (revision 7a6fc957e8ed)
" 2018-03-05 = "add two application examples: depth-first search and 2SAT (revision e5e1a1da2411)" [extra] [related] diff --git a/metadata/entries/Efficient-Mergesort.toml b/metadata/entries/Efficient-Mergesort.toml --- a/metadata/entries/Efficient-Mergesort.toml +++ b/metadata/entries/Efficient-Mergesort.toml @@ -1,38 +1,36 @@ title = "Efficient Mergesort" date = 2011-11-09 topics = [ "Computer science/Algorithms", ] abstract = "We provide a formalization of the mergesort algorithm as used in GHC's Data.List module, proving correctness and stability. Furthermore, experimental data suggests that generated (Haskell-)code for this algorithm is much faster than for previous algorithms available in the Isabelle distribution." license = "bsd" note = "" [authors] [authors.sternagel] email = "sternagel_email" [contributors] [notify] sternagel = "sternagel_email" [history] -2012-10-24 = """ -Added reference to journal article.
-""" +2012-10-24 = "Added reference to journal article.
" 2018-09-17 = """ Added theory Efficient_Mergesort that works exclusively with the mutual induction schemas generated by the function package.
""" 2018-09-19 = """ Theory Efficient_Mergesort replaces theory Efficient_Sort but keeping the old name Efficient_Sort. """ 2020-11-20 = """ Additional theory Natural_Mergesort that developes an efficient mergesort algorithm without key-functions for educational purposes.""" [extra] [related] diff --git a/metadata/entries/Flyspeck-Tame.toml b/metadata/entries/Flyspeck-Tame.toml --- a/metadata/entries/Flyspeck-Tame.toml +++ b/metadata/entries/Flyspeck-Tame.toml @@ -1,37 +1,35 @@ title = "Flyspeck I: Tame Graphs" date = 2006-05-22 topics = [ "Mathematics/Graph theory", ] abstract = """ These theories present the verified enumeration of tame plane graphs as defined by Thomas C. Hales in his proof of the Kepler Conjecture in his book Dense Sphere Packings. A Blueprint for Formal Proofs. [CUP 2012]. The values of the constants in the definition of tameness are identical to those in the Flyspeck project. The IJCAR 2006 paper by Nipkow, Bauer and Schultz refers to the original version of Hales' proof, the ITP 2011 paper by Nipkow refers to the Blueprint version of the proof.""" license = "bsd" note = "" [authors] [authors.bauer] [authors.nipkow] homepage = "nipkow_homepage" [contributors] [notify] nipkow = "nipkow_email" [history] -2010-11-02 = """ -modified theories to reflect the modified definition of tameness in Hales' revised proof.
-""" +2010-11-02 = "modified theories to reflect the modified definition of tameness in Hales' revised proof.
" 2014-07-03 = "modified constants in def of tameness and Archive according to the final state of the Flyspeck proof." [extra] [related] diff --git a/metadata/entries/Interpreter_Optimizations.toml b/metadata/entries/Interpreter_Optimizations.toml --- a/metadata/entries/Interpreter_Optimizations.toml +++ b/metadata/entries/Interpreter_Optimizations.toml @@ -1,40 +1,38 @@ title = "Inline Caching and Unboxing Optimization for Interpreters" date = 2020-12-07 topics = [ "Computer science/Programming languages/Misc", ] abstract = """ This Isabelle/HOL formalization builds on the VeriComp entry of the Archive of Formal Proofs to provide the following contributions:

This formalization was described in the CPP 2021 paper Towards Efficient and Verified Virtual Machines for Dynamic Languages""" license = "bsd" note = "" [authors] [authors.desharnais] homepage = "desharnais_homepage" [contributors] [notify] desharnais = "desharnais_email" [history] -2021-06-14 = """ -refactored function definitions to contain explicit basic blocks
-""" +2021-06-14 = "refactored function definitions to contain explicit basic blocks
" 2021-06-25 = "proved conditional completeness of compilation
" [extra] [related] diff --git a/metadata/entries/Jordan_Normal_Form.toml b/metadata/entries/Jordan_Normal_Form.toml --- a/metadata/entries/Jordan_Normal_Form.toml +++ b/metadata/entries/Jordan_Normal_Form.toml @@ -1,44 +1,42 @@ title = "Matrices, Jordan Normal Forms, and Spectral Radius Theory" date = 2015-08-21 topics = [ "Mathematics/Algebra", ] abstract = """

Matrix interpretations are useful as measure functions in termination proving. In order to use these interpretations also for complexity analysis, the growth rate of matrix powers has to examined. Here, we formalized a central result of spectral radius theory, namely that the growth rate is polynomially bounded if and only if the spectral radius of a matrix is at most one.

To formally prove this result we first studied the growth rates of matrices in Jordan normal form, and prove the result that every complex matrix has a Jordan normal form using a constructive prove via Schur decomposition.

The whole development is based on a new abstract type for matrices, which is also executable by a suitable setup of the code generator. It completely subsumes our former AFP-entry on executable matrices, and its main advantage is its close connection to the HMA-representation which allowed us to easily adapt existing proofs on determinants.

All the results have been applied to improve CeTA, our certifier to validate termination and complexity proof certificates.

""" license = "bsd" note = "" [authors] [authors.thiemann] email = "thiemann_email" [authors.yamada] email = "yamada_email" [contributors] [contributors.bentkamp] email = "bentkamp_email" [notify] thiemann = "thiemann_email" yamada = "yamada_email1" [history] -2016-01-07 = """ -Added Schur-decomposition, Gram-Schmidt orthogonalization, uniqueness of Jordan normal forms
-""" +2016-01-07 = "Added Schur-decomposition, Gram-Schmidt orthogonalization, uniqueness of Jordan normal forms
" 2018-04-17 = "Integrated lemmas from deep-learning AFP-entry of Alexander Bentkamp" [extra] [related] diff --git a/metadata/entries/LLL_Basis_Reduction.toml b/metadata/entries/LLL_Basis_Reduction.toml --- a/metadata/entries/LLL_Basis_Reduction.toml +++ b/metadata/entries/LLL_Basis_Reduction.toml @@ -1,60 +1,58 @@ title = "A verified LLL algorithm" date = 2018-02-02 topics = [ "Computer science/Algorithms/Mathematical", "Mathematics/Algebra", ] abstract = """ The Lenstra-Lenstra-Lovász basis reduction algorithm, also known as LLL algorithm, is an algorithm to find a basis with short, nearly orthogonal vectors of an integer lattice. Thereby, it can also be seen as an approximation to solve the shortest vector problem (SVP), which is an NP-hard problem, where the approximation quality solely depends on the dimension of the lattice, but not the lattice itself. The algorithm also possesses many applications in diverse fields of computer science, from cryptanalysis to number theory, but it is specially well-known since it was used to implement the first polynomial-time algorithm to factor polynomials. In this work we present the first mechanized soundness proof of the LLL algorithm to compute short vectors in lattices. The formalization follows a textbook by von zur Gathen and Gerhard.""" license = "bsd" note = "" [authors] [authors.bottesch] [authors.divason] homepage = "divason_homepage" [authors.haslbeck] homepage = "haslbeck_homepage" [authors.joosten] homepage = "joosten_homepage" [authors.thiemann] homepage = "thiemann_homepage" [authors.yamada] [contributors] [notify] bottesch = "bottesch_email" divason = "divason_email" haslbeck = "haslbeck_email" joosten = "joosten_email2" thiemann = "thiemann_email" yamada = "yamada_email1" [history] -2018-04-16 = """ -Integrated formal complexity bounds (Haslbeck, Thiemann) -""" +2018-04-16 = "Integrated formal complexity bounds (Haslbeck, Thiemann)" 2018-05-25 = "Integrated much faster LLL implementation based on integer arithmetic (Bottesch, Haslbeck, Thiemann)" [extra] [related] diff --git a/metadata/entries/LTL_to_DRA.toml b/metadata/entries/LTL_to_DRA.toml --- a/metadata/entries/LTL_to_DRA.toml +++ b/metadata/entries/LTL_to_DRA.toml @@ -1,28 +1,26 @@ title = "Converting Linear Temporal Logic to Deterministic (Generalized) Rabin Automata" date = 2015-09-04 topics = [ "Computer science/Automata and formal languages", ] abstract = "Recently, Javier Esparza and Jan Kretinsky proposed a new method directly translating linear temporal logic (LTL) formulas to deterministic (generalized) Rabin automata. Compared to the existing approaches of constructing a non-deterministic Buechi-automaton in the first step and then applying a determinization procedure (e.g. some variant of Safra's construction) in a second step, this new approach preservers a relation between the formula and the states of the resulting automaton. While the old approach produced a monolithic structure, the new method is compositional. Furthermore, in some cases the resulting automata are much smaller than the automata generated by existing approaches. In order to ensure the correctness of the construction, this entry contains a complete formalisation and verification of the translation. Furthermore from this basis executable code is generated." license = "bsd" note = "" [authors] [authors.sickert] email = "sickert_email" [contributors] [notify] sickert = "sickert_email" [history] -2015-09-23 = """ -Enable code export for the eager unfolding optimisation and reduce running time of the generated tool. Moreover, add support for the mlton SML compiler.
-""" +2015-09-23 = "Enable code export for the eager unfolding optimisation and reduce running time of the generated tool. Moreover, add support for the mlton SML compiler.
" 2016-03-24 = "Make use of the LTL entry and include the simplifier." [extra] [related] diff --git a/metadata/entries/Launchbury.toml b/metadata/entries/Launchbury.toml --- a/metadata/entries/Launchbury.toml +++ b/metadata/entries/Launchbury.toml @@ -1,28 +1,26 @@ title = "The Correctness of Launchbury's Natural Semantics for Lazy Evaluation" date = 2013-01-31 topics = [ "Computer science/Programming languages/Lambda calculi", "Computer science/Semantics and reasoning", ] abstract = "In his seminal paper \"Natural Semantics for Lazy Evaluation\", John Launchbury proves his semantics correct with respect to a denotational semantics, and outlines an adequacy proof. We have formalized both semantics and machine-checked the correctness proof, clarifying some details. Furthermore, we provide a new and more direct adequacy proof that does not require intermediate operational semantics." license = "bsd" note = "" [authors] [authors.breitner] homepage = "breitner_homepage" [contributors] [notify] [history] -2014-05-24 = """ -Added the proof of adequacy, as well as simplified and improved the existing proofs. Adjusted abstract accordingly. -""" +2014-05-24 = "Added the proof of adequacy, as well as simplified and improved the existing proofs. Adjusted abstract accordingly." 2015-03-16 = "Booleans and if-then-else added to syntax and semantics, making this entry suitable to be used by the entry \"Call_Arity\"." [extra] [related] diff --git a/metadata/entries/Native_Word.toml b/metadata/entries/Native_Word.toml --- a/metadata/entries/Native_Word.toml +++ b/metadata/entries/Native_Word.toml @@ -1,43 +1,41 @@ title = "Native Word" date = 2013-09-17 topics = [ "Computer science/Data structures", ] abstract = "This entry makes machine words and machine arithmetic available for code generation from Isabelle/HOL. It provides a common abstraction that hides the differences between the different target languages. The code generator maps these operations to the APIs of the target languages. Apart from that, we extend the available bit operations on types int and integer, and map them to the operations in the target languages." license = "bsd" note = "" [authors] [authors.lochbihler] homepage = "lochbihler_homepage" [contributors] [contributors.lammich] homepage = "lammich_homepage" [notify] lochbihler = "lochbihler_email1" [history] 2013-11-06 = """ added conversion function between native words and characters (revision fd23d9a7fe3a)
""" 2014-10-06 = """ proper test setup with compilation and execution of tests in all target languages (revision 5d7a1c9ae047)
""" 2018-07-15 = "added cast operators for default-size words (revision fc1f1fb8dd30)
" 2014-03-31 = """ added words of default size in the target language (by Peter Lammich) (revision 25caf5065833)
""" -2017-09-02 = """ -added 64-bit words (revision c89f86244e3c)
-""" +2017-09-02 = "added 64-bit words (revision c89f86244e3c)
" [extra] [related] diff --git a/metadata/entries/Ordinary_Differential_Equations.toml b/metadata/entries/Ordinary_Differential_Equations.toml --- a/metadata/entries/Ordinary_Differential_Equations.toml +++ b/metadata/entries/Ordinary_Differential_Equations.toml @@ -1,58 +1,52 @@ title = "Ordinary Differential Equations" date = 2012-04-26 topics = [ "Mathematics/Analysis", ] abstract = """

Session Ordinary-Differential-Equations formalizes ordinary differential equations (ODEs) and initial value problems. This work comprises proofs for local and global existence of unique solutions (Picard-Lindelöf theorem). Moreover, it contains a formalization of the (continuous or even differentiable) dependency of the flow on initial conditions as the flow of ODEs.

Not in the generated document are the following sessions:

""" license = "bsd" note = "" [authors] [authors.immler] homepage = "immler_homepage" [authors.hoelzl] homepage = "hoelzl_homepage" [contributors] [notify] immler = "immler_email" hoelzl = "hoelzl_email" [history] -2014-02-13 = """ -added an implementation of the Euler method based on affine arithmetic
-""" -2016-04-14 = """ -added flow and variational equation
-""" -2016-08-03 = """ -numerical algorithms for reachability analysis (using second-order Runge-Kutta methods, splitting, and reduction) implemented using Lammich's framework for automatic refinement
-""" +2014-02-13 = "added an implementation of the Euler method based on affine arithmetic
" +2016-04-14 = "added flow and variational equation
" +2016-08-03 = "numerical algorithms for reachability analysis (using second-order Runge-Kutta methods, splitting, and reduction) implemented using Lammich's framework for automatic refinement
" 2017-09-20 = """ added Poincare map and propagation of variational equation in reachability analysis, verified algorithms for C1-information and computations for C0-information of the Lorenz attractor.""" [extra] [related] diff --git a/metadata/entries/Polynomials.toml b/metadata/entries/Polynomials.toml --- a/metadata/entries/Polynomials.toml +++ b/metadata/entries/Polynomials.toml @@ -1,80 +1,76 @@ title = "Executable Multivariate Polynomials" date = 2010-08-10 topics = [ "Mathematics/Analysis", "Mathematics/Algebra", "Computer science/Algorithms/Mathematical", ] abstract = """ We define multivariate polynomials over arbitrary (ordered) semirings in combination with (executable) operations like addition, multiplication, and substitution. We also define (weak) monotonicity of polynomials and comparison of polynomials where we provide standard estimations like absolute positiveness or the more recent approach of Neurauter, Zankl, and Middeldorp. Moreover, it is proven that strongly normalizing (monotone) orders can be lifted to strongly normalizing (monotone) orders over polynomials. Our formalization was performed as part of the IsaFoR/CeTA-system which contains several termination techniques. The provided theories have been essential to formalize polynomial interpretations.

This formalization also contains an abstract representation as coefficient functions with finite support and a type of power-products. If this type is ordered by a linear (term) ordering, various additional notions, such as leading power-product, leading coefficient etc., are introduced as well. Furthermore, a lot of generic properties of, and functions on, multivariate polynomials are formalized, including the substitution and evaluation homomorphisms, embeddings of polynomial rings into larger rings (i.e. with one additional indeterminate), homogenization and dehomogenization of polynomials, and the canonical isomorphism between R[X,Y] and R[X][Y].""" license = "lgpl" note = "" [authors] [authors.sternagel] email = "sternagel_email" [authors.thiemann] homepage = "thiemann_homepage" [authors.maletzky] homepage = "maletzky_homepage" [authors.immler] homepage = "immler_homepage" [authors.haftmann] homepage = "haftmann_homepage" [authors.lochbihler] homepage = "lochbihler_homepage" [authors.bentkamp] email = "bentkamp_email" [contributors] [notify] thiemann = "thiemann_email" sternagel = "sternagel_email1" maletzky = "maletzky_email" immler = "immler_email" [history] -2010-09-17 = """ -Moved theories on arbitrary (ordered) semirings to Abstract Rewriting.
-""" -2016-10-28 = """ -Added abstract representation of polynomials and authors Maletzky/Immler.
-""" +2010-09-17 = "Moved theories on arbitrary (ordered) semirings to Abstract Rewriting.
" +2016-10-28 = "Added abstract representation of polynomials and authors Maletzky/Immler.
" 2018-01-23 = """ Added authors Haftmann, Lochbihler after incorporating their formalization of multivariate polynomials based on Polynomial mappings. Moved material from Bentkamp's entry \"Deep Learning\".
""" 2019-04-18 = """ Added material about polynomials whose power-products are represented themselves by polynomial mappings.""" [extra] [related] diff --git a/metadata/entries/Regular-Sets.toml b/metadata/entries/Regular-Sets.toml --- a/metadata/entries/Regular-Sets.toml +++ b/metadata/entries/Regular-Sets.toml @@ -1,36 +1,34 @@ title = "Regular Sets and Expressions" date = 2010-05-12 topics = [ "Computer science/Automata and formal languages", ] abstract = "This is a library of constructions on regular expressions and languages. It provides the operations of concatenation, Kleene star and derivative on languages. Regular expressions and their meaning are defined. An executable equivalence checker for regular expressions is verified; it does not need automata but works directly on regular expressions. By mapping regular expressions to binary relations, an automatic and complete proof method for (in)equalities of binary relations over union, concatenation and (reflexive) transitive closure is obtained.

Extended regular expressions with complement and intersection are also defined and an equivalence checker is provided." license = "bsd" note = "" [authors] [authors.krauss] homepage = "krauss_homepage" [authors.nipkow] homepage = "nipkow_homepage" [contributors] [contributors.eberl] homepage = "eberl_homepage" [notify] nipkow = "nipkow_email" krauss = "krauss_email" urban = "urban_email" [history] -2011-08-26 = """ -Christian Urban added a theory about derivatives and partial derivatives of regular expressions
-""" +2011-08-26 = "Christian Urban added a theory about derivatives and partial derivatives of regular expressions
" 2012-05-10 = "Tobias Nipkow added equivalence checking with partial derivatives" [extra] [related] diff --git a/metadata/entries/Resolution_FOL.toml b/metadata/entries/Resolution_FOL.toml --- a/metadata/entries/Resolution_FOL.toml +++ b/metadata/entries/Resolution_FOL.toml @@ -1,60 +1,60 @@ title = "The Resolution Calculus for First-Order Logic" date = 2016-06-30 topics = [ "Logic/General logic/Mechanization of proofs", ] abstract = """ This theory is a formalization of the resolution calculus for first-order logic. It is proven sound and complete. The soundness proof uses the substitution lemma, which shows a correspondence between substitutions and updates to an environment. The completeness proof uses semantic trees, i.e. trees whose paths are partial Herbrand interpretations. It employs Herbrand's theorem in a formulation which states that an unsatisfiable set of clauses has a finite closed semantic tree. It also uses the lifting lemma which lifts resolution derivation steps from the ground world up to the first-order world. The theory is presented in a paper in the Journal of Automated Reasoning [Sch18] which extends a paper presented at the International Conference on Interactive Theorem Proving [Sch16]. An earlier version was presented in an MSc thesis [Sch15]. The formalization mostly follows textbooks by Ben-Ari [BA12], Chang and Lee [CL73], and Leitsch [Lei97]. The theory is part of the IsaFoL project [IsaFoL].

[Sch18] Anders Schlichtkrull. \"Formalization of the Resolution Calculus for First-Order Logic\". Journal of Automated Reasoning, 2018.
[Sch16] Anders Schlichtkrull. \"Formalization of the Resolution Calculus for First-Order Logic\". In: ITP 2016. Vol. 9807. LNCS. Springer, 2016.
[Sch15] Anders Schlichtkrull. \"Formalization of Resolution Calculus in Isabelle\". https://people.compute.dtu.dk/andschl/Thesis.pdf. MSc thesis. Technical University of Denmark, 2015.
[BA12] Mordechai Ben-Ari. Mathematical Logic for Computer Science. 3rd. Springer, 2012.
[CL73] Chin-Liang Chang and Richard Char-Tung Lee. Symbolic Logic and Mechanical Theorem Proving. 1st. Academic Press, Inc., 1973.
[Lei97] Alexander Leitsch. The Resolution Calculus. Texts in theoretical computer science. Springer, 1997.
[IsaFoL] IsaFoL authors. IsaFoL: Isabelle Formalization of Logic. https://bitbucket.org/jasmin_blanchette/isafol.""" license = "bsd" note = "" [authors] [authors.schlichtkrull] homepage = "schlichtkrull_homepage" [contributors] [notify] schlichtkrull = "schlichtkrull_email" [history] -2018-01-24 = "added several new versions of the soundness and completeness theorems as described in the paper " -2018-03-20 = "added a concrete instance of the unification and completeness theorems using the First-Order Terms AFP-entry from IsaFoR as described in the papers " +2018-01-24 = "added several new versions of the soundness and completeness theorems as described in the paper" +2018-03-20 = "added a concrete instance of the unification and completeness theorems using the First-Order Terms AFP-entry from IsaFoR as described in the papers" [extra] [related] diff --git a/metadata/entries/Show.toml b/metadata/entries/Show.toml --- a/metadata/entries/Show.toml +++ b/metadata/entries/Show.toml @@ -1,39 +1,37 @@ title = "Haskell's Show Class in Isabelle/HOL" date = 2014-07-29 topics = [ "Computer science/Functional programming", ] abstract = """ We implemented a type class for \"to-string\" functions, 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 show functions for arbitrary user defined datatypes similar to Haskell's \"deriving Show\".""" license = "lgpl" note = "" [authors] [authors.sternagel] email = "sternagel_email" [authors.thiemann] email = "thiemann_email" [contributors] [notify] sternagel = "sternagel_email1" thiemann = "thiemann_email" [history] -2015-03-11 = """ -Adapted development to new-style (BNF-based) datatypes.
-""" +2015-03-11 = "Adapted development to new-style (BNF-based) datatypes.
" 2015-04-10 = """ Moved development for old-style datatypes into subdirectory \"Old_Datatype\".
""" [extra] [related] diff --git a/metadata/entries/Sqrt_Babylonian.toml b/metadata/entries/Sqrt_Babylonian.toml --- a/metadata/entries/Sqrt_Babylonian.toml +++ b/metadata/entries/Sqrt_Babylonian.toml @@ -1,32 +1,30 @@ title = "Computing N-th Roots using the Babylonian Method" date = 2013-01-03 topics = [ "Mathematics/Analysis", ] abstract = """ We implement the Babylonian method to compute n-th roots of numbers. We provide precise algorithms for naturals, integers and rationals, and offer an approximation algorithm for square roots over linear ordered fields. Moreover, there are precise algorithms to compute the floor and the ceiling of n-th roots.""" license = "lgpl" note = "" [authors] [authors.thiemann] email = "thiemann_email" [contributors] [notify] thiemann = "thiemann_email" [history] -2013-10-16 = """ -Added algorithms to compute floor and ceiling of sqrt of integers. -""" +2013-10-16 = "Added algorithms to compute floor and ceiling of sqrt of integers." 2014-07-11 = "Moved NthRoot_Impl from Real-Impl to this entry." [extra] [related] diff --git a/metadata/entries/Well_Quasi_Orders.toml b/metadata/entries/Well_Quasi_Orders.toml --- a/metadata/entries/Well_Quasi_Orders.toml +++ b/metadata/entries/Well_Quasi_Orders.toml @@ -1,60 +1,54 @@ title = "Well-Quasi-Orders" date = 2012-04-13 topics = [ "Mathematics/Combinatorics", ] abstract = """ Based on Isabelle/HOL's type class for preorders, we introduce a type class for well-quasi-orders (wqo) which is characterized by the absence of \"bad\" sequences (our proofs are along the lines of the proof of Nash-Williams, from which we also borrow terminology). Our main results are instantiations for the product type, the list type, and a type of finite trees, which (almost) directly follow from our proofs of (1) Dickson's Lemma, (2) Higman's Lemma, and (3) Kruskal's Tree Theorem. More concretely:

The research was funded by the Austrian Science Fund (FWF): J3202.""" license = "bsd" note = "" [authors] [authors.sternagel] email = "sternagel_email" [contributors] [notify] sternagel = "sternagel_email" [history] -2016-01-03 = """ -An alternative proof of Higman's lemma by open induction.
-""" +2016-01-03 = "An alternative proof of Higman's lemma by open induction.
" 2017-06-08 = """ Proved (classical) equivalence to inductive definition of almost-full relations according to the ITP 2012 paper \"Stop When You Are Almost-Full\" by Vytiniotis, Coquand, and Wahlstedt.""" 2012-12-19 = """ New variant of Kruskal's tree theorem for terms (as opposed to variadic terms, i.e., trees), plus finite version of the tree theorem as corollary.
""" -2013-05-16 = """ -Simplified construction of minimal bad sequences.
-""" +2013-05-16 = "Simplified construction of minimal bad sequences.
" 2014-07-09 = """ Simplified proofs of Higman's lemma and Kruskal's tree theorem, based on homogeneous sequences.
""" -2012-06-11 = """ -Added Kruskal's Tree Theorem.
-""" +2012-06-11 = "Added Kruskal's Tree Theorem.
" [extra] [related]