diff --git a/web/entries/Abstract-Rewriting.html b/web/entries/Abstract-Rewriting.html --- a/web/entries/Abstract-Rewriting.html +++ b/web/entries/Abstract-Rewriting.html @@ -1,277 +1,277 @@ Abstract Rewriting - Archive of Formal Proofs

Abstract Rewriting

Title:	Abstract Rewriting
Authors:	- Christian Sternagel and + Christian Sternagel (c /dot/ sternagel /at/ gmail /dot/ com) and René Thiemann
Submission date:	2010-06-14
Abstract:	We present an Isabelle formalization of abstract rewriting (see, e.g., the book by Baader and Nipkow). First, we define standard relations like joinability, meetability, conversion, etc. Then, we formalize important properties of abstract rewrite systems, e.g., confluence and strong normalization. Our main concern is on strong normalization, since this formalization is the basis of CeTA (which is mainly about strong normalization of term rewrite systems). Hence lemmas involving strong normalization constitute by far the biggest part of this theory. One of those is Newman's lemma.
Change history:	[2010-09-17]: Added theories defining several (ordered) semirings related to strong normalization and giving some standard instances. [2013-10-16]: Generalized delta-orders from rationals to Archimedean fields.
BibTeX:	@article{Abstract-Rewriting-AFP, author = {Christian Sternagel and René Thiemann}, title = {Abstract Rewriting}, journal = {Archive of Formal Proofs}, month = jun, year = 2010, note = {\url{http://isa-afp.org/entries/Abstract-Rewriting.html}, Formal proof development}, ISSN = {2150-914x}, }
License:	GNU Lesser General Public License (LGPL)
Depends on:	Regular-Sets
Used by:	Decreasing-Diagrams, Decreasing-Diagrams-II, First_Order_Terms, Matrix, Minsky_Machines, Myhill-Nerode, Polynomials, Rewriting_Z, Well_Quasi_Orders

Proof outline
Proof document

Browse theories

Download this entry

Older releases:

Isabelle 2019: afp-Abstract-Rewriting-2019-06-11.tar.gz
Isabelle 2018: afp-Abstract-Rewriting-2018-08-16.tar.gz
Isabelle 2017: afp-Abstract-Rewriting-2017-10-10.tar.gz
Isabelle 2016-1: afp-Abstract-Rewriting-2016-12-17.tar.gz
Isabelle 2016: afp-Abstract-Rewriting-2016-02-22.tar.gz
Isabelle 2015: afp-Abstract-Rewriting-2015-05-27.tar.gz
Isabelle 2014: afp-Abstract-Rewriting-2014-08-28.tar.gz
Isabelle 2013-2: afp-Abstract-Rewriting-2013-12-11.tar.gz
Isabelle 2013-1: afp-Abstract-Rewriting-2013-11-17.tar.gz
Isabelle 2013: afp-Abstract-Rewriting-2013-02-16.tar.gz
Isabelle 2012: afp-Abstract-Rewriting-2012-05-24.tar.gz
Isabelle 2011-1: afp-Abstract-Rewriting-2011-10-11.tar.gz
Isabelle 2011: afp-Abstract-Rewriting-2011-02-11.tar.gz
Isabelle 2009-2: afp-Abstract-Rewriting-2010-06-30.tar.gz
Isabelle 2009-1: afp-Abstract-Rewriting-2010-06-17.tar.gz

\ No newline at end of file diff --git a/web/entries/Certification_Monads.html b/web/entries/Certification_Monads.html --- a/web/entries/Certification_Monads.html +++ b/web/entries/Certification_Monads.html @@ -1,220 +1,220 @@ Certification Monads - Archive of Formal Proofs

Certification Monads

Title:	Certification Monads
Authors:	- Christian Sternagel and + Christian Sternagel (c /dot/ sternagel /at/ gmail /dot/ com) and René Thiemann
Submission date:	2014-10-03
Abstract:	This entry provides several monads intended for the development of stand-alone certifiers via code generation from Isabelle/HOL. More specifically, there are three flavors of error monads (the sum type, for the case where all monadic functions are total; an instance of the former, the so called check monad, yielding either success without any further information or an error message; as well as a variant of the sum type that accommodates partial functions by providing an explicit bottom element) and a parser monad built on top. All of this monads are heavily used in the IsaFoR/CeTA project which thus provides many examples of their usage.
BibTeX:	@article{Certification_Monads-AFP, author = {Christian Sternagel and René Thiemann}, title = {Certification Monads}, journal = {Archive of Formal Proofs}, month = oct, year = 2014, note = {\url{http://isa-afp.org/entries/Certification_Monads.html}, Formal proof development}, ISSN = {2150-914x}, }
License:	BSD License
Depends on:	Partial_Function_MR, Show
Used by:	WOOT_Strong_Eventual_Consistency, XML

Proof outline
Proof document

Browse theories

Download this entry

Older releases:

Isabelle 2019: afp-Certification_Monads-2019-06-11.tar.gz
Isabelle 2018: afp-Certification_Monads-2018-08-16.tar.gz
Isabelle 2017: afp-Certification_Monads-2017-10-10.tar.gz
Isabelle 2016-1: afp-Certification_Monads-2016-12-17.tar.gz
Isabelle 2016: afp-Certification_Monads-2016-02-22.tar.gz
Isabelle 2015: afp-Certification_Monads-2015-05-27.tar.gz
Isabelle 2014: afp-Certification_Monads-2014-10-08.tar.gz

\ No newline at end of file diff --git a/web/entries/Deriving.html b/web/entries/Deriving.html --- a/web/entries/Deriving.html +++ b/web/entries/Deriving.html @@ -1,234 +1,234 @@ Deriving class instances for datatypes - Archive of Formal Proofs

Deriving class instances for datatypes

Title:	Deriving class instances for datatypes
Authors:	- Christian Sternagel and + Christian Sternagel (c /dot/ sternagel /at/ gmail /dot/ com) and René Thiemann
Submission date:	2015-03-11
Abstract:	We provide a framework for registering automatic methods to derive class instances of datatypes, as it is possible using Haskell's ``deriving Ord, Show, ...'' feature. We further implemented such automatic methods to derive comparators, linear orders, parametrizable equality functions, and hash-functions which are required in the Isabelle Collection Framework and the Container Framework. Moreover, for the tactic of Blanchette to show that a datatype is countable, we implemented a wrapper so that this tactic becomes accessible in our framework. All of the generators are based on the infrastructure that is provided by the BNF-based datatype package. Our formalization was performed as part of the IsaFoR/CeTA project. With our new tactics we could remove several tedious proofs for (conditional) linear orders, and conditional equality operators within IsaFoR and the Container Framework.
BibTeX:	@article{Deriving-AFP, author = {Christian Sternagel and René Thiemann}, title = {Deriving class instances for datatypes}, journal = {Archive of Formal Proofs}, month = mar, year = 2015, note = {\url{http://isa-afp.org/entries/Deriving.html}, Formal proof development}, ISSN = {2150-914x}, }
License:	BSD License
Depends on:	Collections
Used by:	Affine_Arithmetic, Containers, Datatype_Order_Generator, Formula_Derivatives, Groebner_Bases, LTL_Master_Theorem, MSO_Regex_Equivalence, Real_Impl, Show

Proof outline
Proof document

Browse theories

Download this entry

Older releases:

Isabelle 2019: afp-Deriving-2019-06-11.tar.gz
Isabelle 2018: afp-Deriving-2018-08-16.tar.gz
Isabelle 2017: afp-Deriving-2017-10-10.tar.gz
Isabelle 2016-1: afp-Deriving-2016-12-17.tar.gz
Isabelle 2016: afp-Deriving-2016-02-22.tar.gz
Isabelle 2015: afp-Deriving-2015-05-27.tar.gz

\ No newline at end of file diff --git a/web/entries/Diophantine_Eqns_Lin_Hom.html b/web/entries/Diophantine_Eqns_Lin_Hom.html --- a/web/entries/Diophantine_Eqns_Lin_Hom.html +++ b/web/entries/Diophantine_Eqns_Lin_Hom.html @@ -1,212 +1,212 @@ Homogeneous Linear Diophantine Equations - Archive of Formal Proofs

Homogeneous Linear Diophantine Equations

Title:	Homogeneous Linear Diophantine Equations
Authors:	Florian Messner (florian /dot/ g /dot/ messner /at/ uibk /dot/ ac /dot/ at), Julian Parsert, Jonas Schöpf (jonas /dot/ schoepf /at/ uibk /dot/ ac /dot/ at) and - Christian Sternagel + Christian Sternagel (c /dot/ sternagel /at/ gmail /dot/ com)
Submission date:	2017-10-14
Abstract:	We formalize the theory of homogeneous linear diophantine equations, focusing on two main results: (1) an abstract characterization of minimal complete sets of solutions, and (2) an algorithm computing them. Both, the characterization and the algorithm are based on previous work by Huet. Our starting point is a simple but inefficient variant of Huet's lexicographic algorithm incorporating improved bounds due to Clausen and Fortenbacher. We proceed by proving its soundness and completeness. Finally, we employ code equations to obtain a reasonably efficient implementation. Thus, we provide a formally verified solver for homogeneous linear diophantine equations.
BibTeX:	@article{Diophantine_Eqns_Lin_Hom-AFP, author = {Florian Messner and Julian Parsert and Jonas Schöpf and Christian Sternagel}, title = {Homogeneous Linear Diophantine Equations}, journal = {Archive of Formal Proofs}, month = oct, year = 2017, note = {\url{http://isa-afp.org/entries/Diophantine_Eqns_Lin_Hom.html}, Formal proof development}, ISSN = {2150-914x}, }
License:	GNU Lesser General Public License (LGPL)

Proof outline
Proof document

Browse theories

Download this entry

Older releases:

Isabelle 2019: afp-Diophantine_Eqns_Lin_Hom-2019-06-11.tar.gz
Isabelle 2018: afp-Diophantine_Eqns_Lin_Hom-2018-08-16.tar.gz
Isabelle 2017: afp-Diophantine_Eqns_Lin_Hom-2017-10-15.tar.gz

\ No newline at end of file diff --git a/web/entries/Efficient-Mergesort.html b/web/entries/Efficient-Mergesort.html --- a/web/entries/Efficient-Mergesort.html +++ b/web/entries/Efficient-Mergesort.html @@ -1,261 +1,261 @@ Efficient Mergesort - Archive of Formal Proofs

Efficient Mergesort

Title:	Efficient Mergesort
Author:	- Christian Sternagel + Christian Sternagel (c /dot/ sternagel /at/ gmail /dot/ com)
Submission date:	2011-11-09
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.
Change history:	[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]: Added theory Mergesort_Complexity that proves an upper bound on the number of comparisons that are required by mergesort. [2018-09-19]: Theory Efficient_Mergesort replaces theory Efficient_Sort but keeping the old name Efficient_Sort.
BibTeX:	@article{Efficient-Mergesort-AFP, author = {Christian Sternagel}, title = {Efficient Mergesort}, journal = {Archive of Formal Proofs}, month = nov, year = 2011, note = {\url{http://isa-afp.org/entries/Efficient-Mergesort.html}, Formal proof development}, ISSN = {2150-914x}, }
License:	BSD License
Used by:	Regex_Equivalence

Proof outline
Proof document

Browse theories

Download this entry

Older releases:

Isabelle 2019: afp-Efficient-Mergesort-2019-06-11.tar.gz
Isabelle 2018: afp-Efficient-Mergesort-2018-08-16.tar.gz
Isabelle 2017: afp-Efficient-Mergesort-2017-10-10.tar.gz
Isabelle 2016-1: afp-Efficient-Mergesort-2016-12-17.tar.gz
Isabelle 2016: afp-Efficient-Mergesort-2016-02-22.tar.gz
Isabelle 2015: afp-Efficient-Mergesort-2015-05-27.tar.gz
Isabelle 2014: afp-Efficient-Mergesort-2014-08-28.tar.gz
Isabelle 2013-2: afp-Efficient-Mergesort-2013-12-11.tar.gz
Isabelle 2013-1: afp-Efficient-Mergesort-2013-11-17.tar.gz
Isabelle 2013: afp-Efficient-Mergesort-2013-03-02.tar.gz
Isabelle 2013: afp-Efficient-Mergesort-2013-02-16.tar.gz
Isabelle 2012: afp-Efficient-Mergesort-2012-05-24.tar.gz
Isabelle 2011-1: afp-Efficient-Mergesort-2011-11-10.tar.gz

\ No newline at end of file diff --git a/web/entries/First_Order_Terms.html b/web/entries/First_Order_Terms.html --- a/web/entries/First_Order_Terms.html +++ b/web/entries/First_Order_Terms.html @@ -1,214 +1,214 @@ First-Order Terms - Archive of Formal Proofs

First-Order Terms

Title:	First-Order Terms
Authors:	- Christian Sternagel and + Christian Sternagel (c /dot/ sternagel /at/ gmail /dot/ com) and René Thiemann
Submission date:	2018-02-06
Abstract:	We formalize basic results on first-order terms, including matching and a first-order unification algorithm, as well as well-foundedness of the subsumption order. This entry is part of the Isabelle Formalization of Rewriting IsaFoR, where first-order terms are omni-present: the unification algorithm is used to certify several confluence and termination techniques, like critical-pair computation and dependency graph approximations; and the subsumption order is a crucial ingredient for completion.
BibTeX:	@article{First_Order_Terms-AFP, author = {Christian Sternagel and René Thiemann}, title = {First-Order Terms}, journal = {Archive of Formal Proofs}, month = feb, year = 2018, note = {\url{http://isa-afp.org/entries/First_Order_Terms.html}, Formal proof development}, ISSN = {2150-914x}, }
License:	GNU Lesser General Public License (LGPL)
Depends on:	Abstract-Rewriting
Used by:	Functional_Ordered_Resolution_Prover, Knuth_Bendix_Order, Resolution_FOL

Proof outline
Proof document

Browse theories

Download this entry

Older releases:

Isabelle 2019: afp-First_Order_Terms-2019-06-11.tar.gz
Isabelle 2018: afp-First_Order_Terms-2018-08-16.tar.gz
Isabelle 2017: afp-First_Order_Terms-2018-02-07.tar.gz
Isabelle 2017: afp-First_Order_Terms-2018-02-06.tar.gz

\ No newline at end of file diff --git a/web/entries/Functional_Ordered_Resolution_Prover.html b/web/entries/Functional_Ordered_Resolution_Prover.html --- a/web/entries/Functional_Ordered_Resolution_Prover.html +++ b/web/entries/Functional_Ordered_Resolution_Prover.html @@ -1,217 +1,217 @@ A Verified Functional Implementation of Bachmair and Ganzinger's Ordered Resolution Prover - Archive of Formal Proofs

A Verified Functional Implementation of Bachmair and Ganzinger's Ordered Resolution Prover

- +

Title:	A Verified Functional Implementation of Bachmair and Ganzinger's Ordered Resolution Prover
Authors:	Anders Schlichtkrull, Jasmin Christian Blanchette (j /dot/ c /dot/ blanchette /at/ vu /dot/ nl) and Dmitriy Traytel
Submission date:	2018-11-23
Abstract:	This Isabelle/HOL formalization refines the abstract ordered resolution prover presented in Section 4.3 of Bachmair and Ganzinger's "Resolution Theorem Proving" chapter in the Handbook of Automated Reasoning. The result is a functional implementation of a first-order prover.
BibTeX:	@article{Functional_Ordered_Resolution_Prover-AFP, author = {Anders Schlichtkrull and Jasmin Christian Blanchette and Dmitriy Traytel}, title = {A Verified Functional Implementation of Bachmair and Ganzinger's Ordered Resolution Prover}, journal = {Archive of Formal Proofs}, month = nov, year = 2018, note = {\url{http://isa-afp.org/entries/Functional_Ordered_Resolution_Prover.html}, Formal proof development}, ISSN = {2150-914x}, }
License:	BSD License
Depends on:	First_Order_Terms, Lambda_Free_RPOs, Nested_Multisets_Ordinals, Open_Induction, Ordered_Resolution_Prover, Polynomial_Factorization
First_Order_Terms, Knuth_Bendix_Order, Lambda_Free_RPOs, Nested_Multisets_Ordinals, Open_Induction, Ordered_Resolution_Prover, Polynomial_Factorization

Proof outline
Proof document

Browse theories

Download this entry

Older releases:

Isabelle 2019: afp-Functional_Ordered_Resolution_Prover-2019-06-11.tar.gz
Isabelle 2018: afp-Functional_Ordered_Resolution_Prover-2018-11-29.tar.gz

\ No newline at end of file diff --git a/web/entries/HOLCF-Prelude.html b/web/entries/HOLCF-Prelude.html --- a/web/entries/HOLCF-Prelude.html +++ b/web/entries/HOLCF-Prelude.html @@ -1,208 +1,208 @@ HOLCF-Prelude - Archive of Formal Proofs

HOLCF-Prelude

Title:	HOLCF-Prelude
Authors:	Joachim Breitner (joachim /at/ cis /dot/ upenn /dot/ edu), Brian Huffman, Neil Mitchell and - Christian Sternagel + Christian Sternagel (c /dot/ sternagel /at/ gmail /dot/ com)
Submission date:	2017-07-15
Abstract:	The Isabelle/HOLCF-Prelude is a formalization of a large part of Haskell's standard prelude in Isabelle/HOLCF. We use it to prove the correctness of the Eratosthenes' Sieve, in its self-referential implementation commonly used to showcase Haskell's laziness; prove correctness of GHC's "fold/build" rule and related rewrite rules; and certify a number of hints suggested by HLint.
BibTeX:	@article{HOLCF-Prelude-AFP, author = {Joachim Breitner and Brian Huffman and Neil Mitchell and Christian Sternagel}, title = {HOLCF-Prelude}, journal = {Archive of Formal Proofs}, month = jul, year = 2017, note = {\url{http://isa-afp.org/entries/HOLCF-Prelude.html}, Formal proof development}, ISSN = {2150-914x}, }
License:	BSD License

Proof outline
Proof document

Browse theories

Download this entry

Older releases:

Isabelle 2019: afp-HOLCF-Prelude-2019-06-11.tar.gz
Isabelle 2018: afp-HOLCF-Prelude-2018-08-16.tar.gz
Isabelle 2017: afp-HOLCF-Prelude-2017-10-10.tar.gz
Isabelle 2016-1: afp-HOLCF-Prelude-2017-07-15.tar.gz

\ No newline at end of file diff --git a/web/entries/Imperative_Insertion_Sort.html b/web/entries/Imperative_Insertion_Sort.html --- a/web/entries/Imperative_Insertion_Sort.html +++ b/web/entries/Imperative_Insertion_Sort.html @@ -1,217 +1,217 @@ Imperative Insertion Sort - Archive of Formal Proofs

Imperative Insertion Sort

Title:	Imperative Insertion Sort
Author:	- Christian Sternagel + Christian Sternagel (c /dot/ sternagel /at/ gmail /dot/ com)
Submission date:	2014-09-25
Abstract:	The insertion sort algorithm of Cormen et al. (Introduction to Algorithms) is expressed in Imperative HOL and proved to be correct and terminating. For this purpose we also provide a theory about imperative loop constructs with accompanying induction/invariant rules for proving partial and total correctness. Furthermore, the formalized algorithm is fit for code generation.
BibTeX:	@article{Imperative_Insertion_Sort-AFP, author = {Christian Sternagel}, title = {Imperative Insertion Sort}, journal = {Archive of Formal Proofs}, month = sep, year = 2014, note = {\url{http://isa-afp.org/entries/Imperative_Insertion_Sort.html}, Formal proof development}, ISSN = {2150-914x}, }
License:	BSD License

Proof outline
Proof document

Browse theories

Download this entry

Older releases:

Isabelle 2019: afp-Imperative_Insertion_Sort-2019-06-11.tar.gz
Isabelle 2018: afp-Imperative_Insertion_Sort-2018-08-16.tar.gz
Isabelle 2017: afp-Imperative_Insertion_Sort-2017-10-10.tar.gz
Isabelle 2016-1: afp-Imperative_Insertion_Sort-2016-12-17.tar.gz
Isabelle 2016: afp-Imperative_Insertion_Sort-2016-02-22.tar.gz
Isabelle 2015: afp-Imperative_Insertion_Sort-2015-05-27.tar.gz
Isabelle 2014: afp-Imperative_Insertion_Sort-2014-09-25.tar.gz

\ No newline at end of file diff --git a/web/entries/Knuth_Bendix_Order.html b/web/entries/Knuth_Bendix_Order.html --- a/web/entries/Knuth_Bendix_Order.html +++ b/web/entries/Knuth_Bendix_Order.html @@ -1,193 +1,195 @@ A Formalization of Knuth–Bendix Orders - Archive of Formal Proofs

A Formalization of Knuth–Bendix Orders

- + + +

Title:	A Formalization of Knuth–Bendix Orders
Authors:	- Christian Sternagel and + Christian Sternagel (c /dot/ sternagel /at/ gmail /dot/ com) and René Thiemann
Submission date:	2020-05-13
Abstract:	We define a generalized version of Knuth–Bendix orders, including subterm coefficient functions. For these orders we formalize several properties such as strong normalization, the subterm property, closure properties under substitutions and contexts, as well as ground totality.
BibTeX:	@article{Knuth_Bendix_Order-AFP, author = {Christian Sternagel and René Thiemann}, title = {A Formalization of Knuth–Bendix Orders}, journal = {Archive of Formal Proofs}, month = may, year = 2020, note = {\url{http://isa-afp.org/entries/Knuth_Bendix_Order.html}, Formal proof development}, ISSN = {2150-914x}, }
License:	BSD License
Depends on:	First_Order_Terms, Matrix, Polynomial_Factorization
Used by:	Functional_Ordered_Resolution_Prover

Proof outline
Proof document

Browse theories

Download this entry

Older releases: None

\ No newline at end of file diff --git a/web/entries/Matrix.html b/web/entries/Matrix.html --- a/web/entries/Matrix.html +++ b/web/entries/Matrix.html @@ -1,288 +1,288 @@ Executable Matrix Operations on Matrices of Arbitrary Dimensions - Archive of Formal Proofs

Executable Matrix Operations on Matrices of Arbitrary Dimensions

Title:	Executable Matrix Operations on Matrices of Arbitrary Dimensions
Authors:	- Christian Sternagel and + Christian Sternagel (c /dot/ sternagel /at/ gmail /dot/ com) and René Thiemann
Submission date:	2010-06-17
Abstract:	We provide the operations of matrix addition, multiplication, transposition, and matrix comparisons as executable functions over ordered semirings. Moreover, it is proven that strongly normalizing (monotone) orders can be lifted to strongly normalizing (monotone) orders over matrices. We further show that the standard semirings over the naturals, integers, and rationals, as well as the arctic semirings satisfy the axioms that are required by our matrix theory. Our formalization is part of the CeTA system which contains several termination techniques. The provided theories have been essential to formalize matrix-interpretations and arctic interpretations.
Change history:	[2010-09-17]: Moved theory on arbitrary (ordered) semirings to Abstract Rewriting.
BibTeX:	@article{Matrix-AFP, author = {Christian Sternagel and René Thiemann}, title = {Executable Matrix Operations on Matrices of Arbitrary Dimensions}, journal = {Archive of Formal Proofs}, month = jun, year = 2010, note = {\url{http://isa-afp.org/entries/Matrix.html}, Formal proof development}, ISSN = {2150-914x}, }
License:	GNU Lesser General Public License (LGPL)
Depends on:	Abstract-Rewriting
Used by:	Knuth_Bendix_Order, Matrix_Tensor, Polynomials, Transitive-Closure

Proof outline
Proof document

Browse theories

Download this entry

Older releases:

Isabelle 2019: afp-Matrix-2019-06-11.tar.gz
Isabelle 2018: afp-Matrix-2018-08-16.tar.gz
Isabelle 2017: afp-Matrix-2017-10-10.tar.gz
Isabelle 2016-1: afp-Matrix-2016-12-17.tar.gz
Isabelle 2016: afp-Matrix-2016-02-22.tar.gz
Isabelle 2015: afp-Matrix-2015-05-27.tar.gz
Isabelle 2014: afp-Matrix-2014-08-28.tar.gz
Isabelle 2013-2: afp-Matrix-2013-12-11.tar.gz
Isabelle 2013-1: afp-Matrix-2013-11-17.tar.gz
Isabelle 2013: afp-Matrix-2013-02-16.tar.gz
Isabelle 2012: afp-Matrix-2012-05-24.tar.gz
Isabelle 2011-1: afp-Matrix-2011-10-11.tar.gz
Isabelle 2011: afp-Matrix-2011-02-11.tar.gz
Isabelle 2009-2: afp-Matrix-2010-07-01.tar.gz
Isabelle 2009-1: afp-Matrix-2010-06-17.tar.gz

\ No newline at end of file diff --git a/web/entries/Open_Induction.html b/web/entries/Open_Induction.html --- a/web/entries/Open_Induction.html +++ b/web/entries/Open_Induction.html @@ -1,240 +1,240 @@ Open Induction - Archive of Formal Proofs

Open Induction

Title:	Open Induction
Authors:	Mizuhito Ogawa and - Christian Sternagel + Christian Sternagel (c /dot/ sternagel /at/ gmail /dot/ com)
Submission date:	2012-11-02
Abstract:	A proof of the open induction schema based on J.-C. Raoult, Proving open properties by induction, Information Processing Letters 29, 1988, pp.19-23. This research was supported by the Austrian Science Fund (FWF): J3202.
BibTeX:	@article{Open_Induction-AFP, author = {Mizuhito Ogawa and Christian Sternagel}, title = {Open Induction}, journal = {Archive of Formal Proofs}, month = nov, year = 2012, note = {\url{http://isa-afp.org/entries/Open_Induction.html}, Formal proof development}, ISSN = {2150-914x}, }
License:	BSD License
Used by:	Decreasing-Diagrams-II, Functional_Ordered_Resolution_Prover, Myhill-Nerode, Well_Quasi_Orders

Proof outline
Proof document

Browse theories

Download this entry

Older releases:

Isabelle 2019: afp-Open_Induction-2019-06-11.tar.gz
Isabelle 2018: afp-Open_Induction-2018-08-16.tar.gz
Isabelle 2017: afp-Open_Induction-2017-10-10.tar.gz
Isabelle 2016-1: afp-Open_Induction-2016-12-17.tar.gz
Isabelle 2016: afp-Open_Induction-2016-02-22.tar.gz
Isabelle 2015: afp-Open_Induction-2015-05-27.tar.gz
Isabelle 2014: afp-Open_Induction-2014-08-28.tar.gz
Isabelle 2013-2: afp-Open_Induction-2013-12-11.tar.gz
Isabelle 2013-1: afp-Open_Induction-2013-11-17.tar.gz
Isabelle 2013: afp-Open_Induction-2013-03-02.tar.gz
Isabelle 2013: afp-Open_Induction-2013-02-16.tar.gz

\ No newline at end of file diff --git a/web/entries/Polynomials.html b/web/entries/Polynomials.html --- a/web/entries/Polynomials.html +++ b/web/entries/Polynomials.html @@ -1,296 +1,296 @@ Executable Multivariate Polynomials - Archive of Formal Proofs

Executable Multivariate Polynomials

Title:	Executable Multivariate Polynomials
Authors:	- Christian Sternagel, + Christian Sternagel (c /dot/ sternagel /at/ gmail /dot/ com), René Thiemann, Alexander Maletzky, Fabian Immler, Florian Haftmann, Andreas Lochbihler and Alexander Bentkamp (bentkamp /at/ gmail /dot/ com)
Submission date:	2010-08-10
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].
Change 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. [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.
BibTeX:	@article{Polynomials-AFP, author = {Christian Sternagel and René Thiemann and Alexander Maletzky and Fabian Immler and Florian Haftmann and Andreas Lochbihler and Alexander Bentkamp}, title = {Executable Multivariate Polynomials}, journal = {Archive of Formal Proofs}, month = aug, year = 2010, note = {\url{http://isa-afp.org/entries/Polynomials.html}, Formal proof development}, ISSN = {2150-914x}, }
License:	GNU Lesser General Public License (LGPL)
Depends on:	Abstract-Rewriting, Matrix, Show, Well_Quasi_Orders
Used by:	Deep_Learning, Groebner_Bases, Lambda_Free_KBOs, Symmetric_Polynomials

Proof outline
Proof document

Browse theories

Download this entry

Older releases:

Isabelle 2019: afp-Polynomials-2020-01-14.tar.gz
Isabelle 2019: afp-Polynomials-2019-06-11.tar.gz
Isabelle 2018: afp-Polynomials-2018-08-16.tar.gz
Isabelle 2017: afp-Polynomials-2017-10-10.tar.gz
Isabelle 2016-1: afp-Polynomials-2016-12-17.tar.gz
Isabelle 2016: afp-Polynomials-2016-02-22.tar.gz
Isabelle 2015: afp-Polynomials-2015-05-27.tar.gz
Isabelle 2014: afp-Polynomials-2014-08-28.tar.gz
Isabelle 2013-2: afp-Polynomials-2013-12-11.tar.gz
Isabelle 2013-1: afp-Polynomials-2013-11-17.tar.gz
Isabelle 2013: afp-Polynomials-2013-02-16.tar.gz
Isabelle 2012: afp-Polynomials-2012-05-24.tar.gz
Isabelle 2011-1: afp-Polynomials-2011-10-11.tar.gz
Isabelle 2011: afp-Polynomials-2011-02-11.tar.gz
Isabelle 2009-2: afp-Polynomials-2010-08-11.tar.gz

\ No newline at end of file diff --git a/web/entries/Rewriting_Z.html b/web/entries/Rewriting_Z.html --- a/web/entries/Rewriting_Z.html +++ b/web/entries/Rewriting_Z.html @@ -1,217 +1,217 @@ The Z Property - Archive of Formal Proofs

The Z Property

Title:	The Z Property
Authors:	Bertram Felgenhauer (int-e /at/ gmx /dot/ de), Julian Nagele, Vincent van Oostrom and - Christian Sternagel + Christian Sternagel (c /dot/ sternagel /at/ gmail /dot/ com)
Submission date:	2016-06-30
Abstract:	We formalize the Z property introduced by Dehornoy and van Oostrom. First we show that for any abstract rewrite system, Z implies confluence. Then we give two examples of proofs using Z: confluence of lambda-calculus with respect to beta-reduction and confluence of combinatory logic.
BibTeX:	@article{Rewriting_Z-AFP, author = {Bertram Felgenhauer and Julian Nagele and Vincent van Oostrom and Christian Sternagel}, title = {The Z Property}, journal = {Archive of Formal Proofs}, month = jun, year = 2016, note = {\url{http://isa-afp.org/entries/Rewriting_Z.html}, Formal proof development}, ISSN = {2150-914x}, }
License:	BSD License
Depends on:	Abstract-Rewriting, Nominal2

Proof outline
Proof document

Browse theories

Download this entry

Older releases:

Isabelle 2019: afp-Rewriting_Z-2019-06-11.tar.gz
Isabelle 2018: afp-Rewriting_Z-2018-08-16.tar.gz
Isabelle 2017: afp-Rewriting_Z-2017-10-10.tar.gz
Isabelle 2016-1: afp-Rewriting_Z-2016-12-17.tar.gz
Isabelle 2016: afp-Rewriting_Z-2016-06-30.tar.gz

\ No newline at end of file diff --git a/web/entries/Show.html b/web/entries/Show.html --- a/web/entries/Show.html +++ b/web/entries/Show.html @@ -1,242 +1,242 @@ Haskell's Show Class in Isabelle/HOL - Archive of Formal Proofs

Haskell's Show Class in Isabelle/HOL

Title:	Haskell's Show Class in Isabelle/HOL
Authors:	- Christian Sternagel and + Christian Sternagel (c /dot/ sternagel /at/ gmail /dot/ com) and René Thiemann
Submission date:	2014-07-29
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".
Change history:	[2015-03-11]: Adapted development to new-style (BNF-based) datatypes. [2015-04-10]: Moved development for old-style datatypes into subdirectory "Old_Datatype".
BibTeX:	@article{Show-AFP, author = {Christian Sternagel and René Thiemann}, title = {Haskell's Show Class in Isabelle/HOL}, journal = {Archive of Formal Proofs}, month = jul, year = 2014, note = {\url{http://isa-afp.org/entries/Show.html}, Formal proof development}, ISSN = {2150-914x}, }
License:	GNU Lesser General Public License (LGPL)
Depends on:	Deriving
Used by:	Affine_Arithmetic, CakeML, CakeML_Codegen, Certification_Monads, Dict_Construction, Monad_Memo_DP, Polynomial_Factorization, Polynomials, Real_Impl, XML

Proof outline
Proof document

Browse theories

Download this entry

Older releases:

Isabelle 2019: afp-Show-2019-06-11.tar.gz
Isabelle 2018: afp-Show-2018-08-16.tar.gz
Isabelle 2017: afp-Show-2017-10-10.tar.gz
Isabelle 2016-1: afp-Show-2016-12-17.tar.gz
Isabelle 2016: afp-Show-2016-02-22.tar.gz
Isabelle 2015: afp-Show-2015-05-27.tar.gz
Isabelle 2014: afp-Show-2014-08-29.tar.gz
Isabelle 2014: afp-Show-2014-08-28.tar.gz

\ No newline at end of file diff --git a/web/entries/Transitive-Closure.html b/web/entries/Transitive-Closure.html --- a/web/entries/Transitive-Closure.html +++ b/web/entries/Transitive-Closure.html @@ -1,267 +1,267 @@ Executable Transitive Closures of Finite Relations - Archive of Formal Proofs

Executable Transitive Closures of Finite Relations

Title:	Executable Transitive Closures of Finite Relations
Authors:	- Christian Sternagel and + Christian Sternagel (c /dot/ sternagel /at/ gmail /dot/ com) and René Thiemann
Submission date:	2011-03-14
Abstract:	We provide a generic work-list algorithm to compute the transitive closure of finite relations where only successors of newly detected states are generated. This algorithm is then instantiated for lists over arbitrary carriers and red black trees (which are faster but require a linear order on the carrier), respectively. Our formalization was performed as part of the IsaFoR/CeTA project where reflexive transitive closures of large tree automata have to be computed.
Change history:	[2014-09-04] added example simprocs in Finite_Transitive_Closure_Simprocs
BibTeX:	@article{Transitive-Closure-AFP, author = {Christian Sternagel and René Thiemann}, title = {Executable Transitive Closures of Finite Relations}, journal = {Archive of Formal Proofs}, month = mar, year = 2011, note = {\url{http://isa-afp.org/entries/Transitive-Closure.html}, Formal proof development}, ISSN = {2150-914x}, }
License:	GNU Lesser General Public License (LGPL)
Depends on:	Collections, Matrix
Used by:	KBPs, Network_Security_Policy_Verification, Planarity_Certificates

Proof outline
Proof document

Browse theories

Download this entry

Older releases:

Isabelle 2019: afp-Transitive-Closure-2019-06-11.tar.gz
Isabelle 2018: afp-Transitive-Closure-2018-08-16.tar.gz
Isabelle 2017: afp-Transitive-Closure-2017-10-10.tar.gz
Isabelle 2016-1: afp-Transitive-Closure-2016-12-17.tar.gz
Isabelle 2016: afp-Transitive-Closure-2016-02-22.tar.gz
Isabelle 2015: afp-Transitive-Closure-2015-05-27.tar.gz
Isabelle 2014: afp-Transitive-Closure-2014-08-28.tar.gz
Isabelle 2013-2: afp-Transitive-Closure-2013-12-11.tar.gz
Isabelle 2013-1: afp-Transitive-Closure-2013-11-17.tar.gz
Isabelle 2013: afp-Transitive-Closure-2013-02-16.tar.gz
Isabelle 2012: afp-Transitive-Closure-2012-05-24.tar.gz
Isabelle 2011-1: afp-Transitive-Closure-2011-10-12.tar.gz
Isabelle 2011-1: afp-Transitive-Closure-2011-10-11.tar.gz
Isabelle 2011: afp-Transitive-Closure-2011-03-14.tar.gz

\ No newline at end of file diff --git a/web/entries/Well_Quasi_Orders.html b/web/entries/Well_Quasi_Orders.html --- a/web/entries/Well_Quasi_Orders.html +++ b/web/entries/Well_Quasi_Orders.html @@ -1,264 +1,264 @@ Well-Quasi-Orders - Archive of Formal Proofs

Well-Quasi-Orders

Title:	Well-Quasi-Orders
Author:	- Christian Sternagel + Christian Sternagel (c /dot/ sternagel /at/ gmail /dot/ com)
Submission date:	2012-04-13
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: If the sets A and B are wqo then their Cartesian product is wqo. If the set A is wqo then the set of finite lists over A is wqo. If the set A is wqo then the set of finite trees over A is wqo. The research was funded by the Austrian Science Fund (FWF): J3202.
Change history:	[2012-06-11]: Added Kruskal's Tree Theorem. [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. [2014-07-09]: Simplified proofs of Higman's lemma and Kruskal's tree theorem, based on homogeneous sequences. [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.
BibTeX:	@article{Well_Quasi_Orders-AFP, author = {Christian Sternagel}, title = {Well-Quasi-Orders}, journal = {Archive of Formal Proofs}, month = apr, year = 2012, note = {\url{http://isa-afp.org/entries/Well_Quasi_Orders.html}, Formal proof development}, ISSN = {2150-914x}, }
License:	BSD License
Depends on:	Abstract-Rewriting, Open_Induction
Used by:	Decreasing-Diagrams-II, Myhill-Nerode, Polynomials, Saturation_Framework

Proof outline
Proof document

Browse theories

Download this entry

Older releases:

Isabelle 2019: afp-Well_Quasi_Orders-2019-06-11.tar.gz
Isabelle 2018: afp-Well_Quasi_Orders-2018-08-16.tar.gz
Isabelle 2017: afp-Well_Quasi_Orders-2017-10-10.tar.gz
Isabelle 2016-1: afp-Well_Quasi_Orders-2016-12-17.tar.gz
Isabelle 2016: afp-Well_Quasi_Orders-2016-02-22.tar.gz
Isabelle 2015: afp-Well_Quasi_Orders-2015-05-27.tar.gz
Isabelle 2014: afp-Well_Quasi_Orders-2014-08-28.tar.gz
Isabelle 2013-2: afp-Well_Quasi_Orders-2013-12-11.tar.gz
Isabelle 2013-1: afp-Well_Quasi_Orders-2013-11-17.tar.gz
Isabelle 2013: afp-Well_Quasi_Orders-2013-02-16.tar.gz
Isabelle 2012: afp-Well_Quasi_Orders-2012-05-24.tar.gz

\ No newline at end of file diff --git a/web/entries/XML.html b/web/entries/XML.html --- a/web/entries/XML.html +++ b/web/entries/XML.html @@ -1,223 +1,223 @@ XML - Archive of Formal Proofs

XML

Title:	XML
Authors:	- Christian Sternagel and + Christian Sternagel (c /dot/ sternagel /at/ gmail /dot/ com) and René Thiemann
Submission date:	2014-10-03
Abstract:	This entry provides an XML library for Isabelle/HOL. This includes parsing and pretty printing of XML trees as well as combinators for transforming XML trees into arbitrary user-defined data. The main contribution of this entry is an interface (fit for code generation) that allows for communication between verified programs formalized in Isabelle/HOL and the outside world via XML. This library was developed as part of the IsaFoR/CeTA project to which we refer for examples of its usage.
BibTeX:	@article{XML-AFP, author = {Christian Sternagel and René Thiemann}, title = {XML}, journal = {Archive of Formal Proofs}, month = oct, year = 2014, note = {\url{http://isa-afp.org/entries/XML.html}, Formal proof development}, ISSN = {2150-914x}, }
License:	BSD License
Depends on:	Certification_Monads, Show

Proof outline
Proof document

Browse theories

Download this entry

Older releases:

Isabelle 2019: afp-XML-2019-06-11.tar.gz
Isabelle 2018: afp-XML-2018-08-16.tar.gz
Isabelle 2017: afp-XML-2017-10-10.tar.gz
Isabelle 2016-1: afp-XML-2016-12-17.tar.gz
Isabelle 2016: afp-XML-2016-02-22.tar.gz
Isabelle 2015: afp-XML-2015-05-27.tar.gz
Isabelle 2014: afp-XML-2014-10-08.tar.gz

\ No newline at end of file diff --git a/web/statistics.html b/web/statistics.html --- a/web/statistics.html +++ b/web/statistics.html @@ -1,303 +1,303 @@ Archive of Formal Proofs

Statistics

- +

Number of Articles:	531
Number of Authors:	350
Number of lemmas:	~143,700
Lines of Code:	~2,494,600
Lines of Code:	~2,493,800

Most used AFP articles:

	Name	Used by ? articles
1.	List-Index	14
2.	Coinductive	12
	Collections	12
	Regular-Sets	12
3.	Landau_Symbols	11
4.	Show	10
5.	Abstract-Rewriting	9
	Automatic_Refinement	9
	Deriving	9
6.	Jordan_Normal_Form	8
	Native_Word	8

Abstract Rewriting

Certification Monads

Deriving class instances for datatypes

Homogeneous Linear Diophantine Equations

Efficient Mergesort

First-Order Terms

A Verified Functional Implementation of Bachmair and Ganzinger's Ordered Resolution Prover

HOLCF-Prelude

Imperative Insertion Sort

A Formalization of Knuth–Bendix Orders

Executable Matrix Operations on Matrices of Arbitrary Dimensions

Open Induction

Executable Multivariate Polynomials

The Z Property

Haskell's Show Class in Isabelle/HOL

Executable Transitive Closures of Finite Relations

Well-Quasi-Orders

XML

Statistics

Statistics

Most used AFP articles:

Growth in number of articles:

Growth in lines of code:

Growth in number of authors:

Size of articles: