diff --git a/web/entries/Affine_Arithmetic.html b/web/entries/Affine_Arithmetic.html --- a/web/entries/Affine_Arithmetic.html +++ b/web/entries/Affine_Arithmetic.html @@ -1,221 +1,220 @@ Affine Arithmetic - Archive of Formal Proofs

Affine Arithmetic

Fabian Immler 🌐

February 7, 2014

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.
BSD License

Change history

September 20, 2017

linear approximations for all symbols from the floatarith data type

January 31, 2015

added algorithm for zonotope/hyperplane intersection
-

Topics

Theories of Affine_Arithmetic

Depends On

Used by

Related Entries

Cite

× 
@article{Affine_Arithmetic-AFP,
   author  = {Fabian Immler},
   title   = {Affine Arithmetic},
   journal = {Archive of Formal Proofs},
   month   = {February},
   year    = {2014},
   note    = {\url{https://isa-afp.org/entries/Affine_Arithmetic.html},
             Formal proof development},
   ISSN    = {2150-914x},
 }
Download

Download

× Download latest

Older releases:

\ No newline at end of file diff --git a/web/entries/Algebraic_Numbers.html b/web/entries/Algebraic_Numbers.html --- a/web/entries/Algebraic_Numbers.html +++ b/web/entries/Algebraic_Numbers.html @@ -1,223 +1,222 @@ Algebraic Numbers in Isabelle/HOL - Archive of Formal Proofs

Algebraic Numbers in Isabelle/HOL

René Thiemann 📧, Akihisa Yamada 📧 and Sebastiaan J. C. Joosten 📧 with contributions from Manuel Eberl 🌐

December 22, 2015

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.

BSD License

Change history

April 16, 2017

Use certified Berlekamp-Zassenhaus factorization, use subresultant algorithm for computing resultants, improved bisection algorithm

January 29, 2016

Split off Polynomial Interpolation and Polynomial Factorization
-

Topics

Theories of Algebraic_Numbers

Depends On

Used by

Related Entries

Cite

× 
@article{Algebraic_Numbers-AFP,
   author  = {René Thiemann and Akihisa Yamada and Sebastiaan J. C. Joosten},
   title   = {Algebraic Numbers in Isabelle/HOL},
   journal = {Archive of Formal Proofs},
   month   = {December},
   year    = {2015},
   note    = {\url{https://isa-afp.org/entries/Algebraic_Numbers.html},
             Formal proof development},
   ISSN    = {2150-914x},
 }
Download

Download

× Download latest

Older releases:

\ No newline at end of file diff --git a/web/entries/Amortized_Complexity.html b/web/entries/Amortized_Complexity.html --- a/web/entries/Amortized_Complexity.html +++ b/web/entries/Amortized_Complexity.html @@ -1,228 +1,226 @@ Amortized Complexity Verified - Archive of Formal Proofs

Amortized Complexity Verified

Tobias Nipkow 🌐

July 7, 2014

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.

BSD License

Change history

July 14, 2016

Moved pairing heaps from here to the new Pairing_Heap

July 12, 2016

Moved splay heaps from here to Splay_Tree
-

March 17, 2015

Added pairing heaps by Hauke Brinkop.
-

Topics

Theories of Amortized_Complexity

Depends On

Used by

Related Entries

Cite

× 
@article{Amortized_Complexity-AFP,
   author  = {Tobias Nipkow},
   title   = {Amortized Complexity Verified},
   journal = {Archive of Formal Proofs},
   month   = {July},
   year    = {2014},
   note    = {\url{https://isa-afp.org/entries/Amortized_Complexity.html},
             Formal proof development},
   ISSN    = {2150-914x},
 }
Download

Download

× Download latest

Older releases:

\ No newline at end of file diff --git a/web/entries/Applicative_Lifting.html b/web/entries/Applicative_Lifting.html --- a/web/entries/Applicative_Lifting.html +++ b/web/entries/Applicative_Lifting.html @@ -1,218 +1,217 @@ Applicative Lifting - Archive of Formal Proofs

Applicative Lifting

Andreas Lochbihler 🌐 and Joshua Schneider

December 22, 2015

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.

BSD License

Change history

June 10, 2016

implemented automatic derivation of lifted combinator reductions; support arbitrary lifted relations using relators; improved compatibility with locale interpretation (revision ec336f354f37)

March 3, 2016

added formalisation of lifting with combinators
-

Topics

Theories of Applicative_Lifting

Used by

Cite

× 
@article{Applicative_Lifting-AFP,
   author  = {Andreas Lochbihler and Joshua Schneider},
   title   = {Applicative Lifting},
   journal = {Archive of Formal Proofs},
   month   = {December},
   year    = {2015},
   note    = {\url{https://isa-afp.org/entries/Applicative_Lifting.html},
             Formal proof development},
   ISSN    = {2150-914x},
 }
Download

Download

× Download latest

Older releases:

\ No newline at end of file diff --git a/web/entries/Approximation_Algorithms.html b/web/entries/Approximation_Algorithms.html --- a/web/entries/Approximation_Algorithms.html +++ b/web/entries/Approximation_Algorithms.html @@ -1,179 +1,178 @@ Verified Approximation Algorithms - Archive of Formal Proofs

Verified Approximation Algorithms

Robin Eßmann 📧, Tobias Nipkow 🌐, Simon Robillard 🌐 and Ujkan Sulejmani

January 16, 2020

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.
BSD License

Change history

June 29, 2021

added theory Center_Selection by Ujkan Sulejmani

February 8, 2021

added theory Approx_SC_Hoare (Set Cover) by Robin Eßmann
-

Topics

Theories of Approximation_Algorithms

Cite

× 
@article{Approximation_Algorithms-AFP,
   author  = {Robin Eßmann and Tobias Nipkow and Simon Robillard and Ujkan Sulejmani},
   title   = {Verified Approximation Algorithms},
   journal = {Archive of Formal Proofs},
   month   = {January},
   year    = {2020},
   note    = {\url{https://isa-afp.org/entries/Approximation_Algorithms.html},
             Formal proof development},
   ISSN    = {2150-914x},
 }
Download

Download

× Download latest

Older releases:

\ No newline at end of file diff --git a/web/entries/Architectural_Design_Patterns.html b/web/entries/Architectural_Design_Patterns.html --- a/web/entries/Architectural_Design_Patterns.html +++ b/web/entries/Architectural_Design_Patterns.html @@ -1,196 +1,195 @@ A Theory of Architectural Design Patterns - Archive of Formal Proofs

A Theory of Architectural Design Patterns

Diego Marmsoler 🌐

March 1, 2018

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.
BSD License

Change history

April 8, 2019

adapting the terminology: honest instead of trusted, dishonest instead of untrusted (revision 7af3431a22ae)

May 25, 2018

changing the major assumption for blockchain architectures from alternative minings to relative mining frequencies (revision 5043c5c71685)
-

Topics

Theories of Architectural_Design_Patterns

Depends On

Cite

× 
@article{Architectural_Design_Patterns-AFP,
   author  = {Diego Marmsoler},
   title   = {A Theory of Architectural Design Patterns},
   journal = {Archive of Formal Proofs},
   month   = {March},
   year    = {2018},
   note    = {\url{https://isa-afp.org/entries/Architectural_Design_Patterns.html},
             Formal proof development},
   ISSN    = {2150-914x},
 }
Download

Download

× Download latest

Older releases:

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

Collections Framework

Peter Lammich 🌐 with contributions from Andreas Lochbihler 🌐 and Thomas Tuerk

November 25, 2009

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.
BSD License

Change history

April 25, 2012

New iterator foundation by Tuerk. Various maintenance changes.
-

October 10, 2011

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

December 1, 2010

New Interfaces: Priority Queues, Annotated Lists. Implemented by finger trees, (skew) binomial queues.
-

October 8, 2010

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.

Topics

Theories of Collections

Theories of Collections_Examples

Depends On

Used by

Related Entries

Cite

× 
@article{Collections-AFP,
   author  = {Peter Lammich},
   title   = {Collections Framework},
   journal = {Archive of Formal Proofs},
   month   = {November},
   year    = {2009},
   note    = {\url{https://isa-afp.org/entries/Collections.html},
             Formal proof development},
   ISSN    = {2150-914x},
 }
Download

Download

× Download latest

Older releases:

\ No newline at end of file diff --git a/web/entries/Containers.html b/web/entries/Containers.html --- a/web/entries/Containers.html +++ b/web/entries/Containers.html @@ -1,264 +1,262 @@ Light-weight Containers - Archive of Formal Proofs

Light-Weight Containers

Andreas Lochbihler 🌐 with contributions from René Thiemann 📧

April 15, 2013

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.

BSD License

Change history

March 5, 2018

add two application examples: depth-first search and 2SAT (revision e5e1a1da2411)

July 8, 2014

add support for going from partial functions to mappings (revision 7a6fc957e8ed)
-

September 20, 2013

provide generators for canonical type class instantiations (revision 159f4401f4a8 by René Thiemann)

July 11, 2013

add pretty printing for sets (revision 7f3f52c5f5fa)
-

Topics

Theories of Containers

Theories of Containers-Benchmarks

Depends On

Used by

Related Entries

Cite

× 
@article{Containers-AFP,
   author  = {Andreas Lochbihler},
   title   = {Light-weight Containers},
   journal = {Archive of Formal Proofs},
   month   = {April},
   year    = {2013},
   note    = {\url{https://isa-afp.org/entries/Containers.html},
             Formal proof development},
   ISSN    = {2150-914x},
 }
Download

Download

× Download latest

Older releases:

\ 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,209 +1,208 @@ Efficient Mergesort - Archive of Formal Proofs

Efficient Mergesort

Christian Sternagel 📧

November 9, 2011

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.
BSD License

Change history

November 20, 2020

Additional theory Natural_Mergesort that developes an efficient mergesort algorithm without key-functions for educational purposes.

September 19, 2018

Theory Efficient_Mergesort replaces theory Efficient_Sort but keeping the old name Efficient_Sort.

September 17, 2018

Added theory Efficient_Mergesort that works exclusively with the mutual induction schemas generated by the function package.

October 24, 2012

Added reference to journal article.
-

Topics

Theories of Efficient-Mergesort

Used by

Cite

× 
@article{Efficient-Mergesort-AFP,
   author  = {Christian Sternagel},
   title   = {Efficient Mergesort},
   journal = {Archive of Formal Proofs},
   month   = {November},
   year    = {2011},
   note    = {\url{https://isa-afp.org/entries/Efficient-Mergesort.html},
             Formal proof development},
   ISSN    = {2150-914x},
 }
Download

Download

× Download latest

Older releases:

\ No newline at end of file diff --git a/web/entries/Flyspeck-Tame.html b/web/entries/Flyspeck-Tame.html --- a/web/entries/Flyspeck-Tame.html +++ b/web/entries/Flyspeck-Tame.html @@ -1,263 +1,262 @@ Flyspeck I: Tame Graphs - Archive of Formal Proofs

Flyspeck I: Tame Graphs

Gertrud Bauer and Tobias Nipkow 🌐

May 22, 2006

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.
BSD License

Change history

July 3, 2014

modified constants in def of tameness and Archive according to the final state of the Flyspeck proof.

November 2, 2010

modified theories to reflect the modified definition of tameness in Hales' revised proof.
-

Topics

Theories of Flyspeck-Tame

Theories of Flyspeck-Tame-Computation

Depends On

Used by

Related Entries

Cite

× 
@article{Flyspeck-Tame-AFP,
   author  = {Gertrud Bauer and Tobias Nipkow},
   title   = {Flyspeck I: Tame Graphs},
   journal = {Archive of Formal Proofs},
   month   = {May},
   year    = {2006},
   note    = {\url{https://isa-afp.org/entries/Flyspeck-Tame.html},
             Formal proof development},
   ISSN    = {2150-914x},
 }
Download

Download

× Download latest

Older releases:

\ No newline at end of file diff --git a/web/entries/Interpreter_Optimizations.html b/web/entries/Interpreter_Optimizations.html --- a/web/entries/Interpreter_Optimizations.html +++ b/web/entries/Interpreter_Optimizations.html @@ -1,202 +1,201 @@ Inline Caching and Unboxing Optimization for Interpreters - Archive of Formal Proofs

Inline Caching and Unboxing Optimization for Interpreters

Martin Desharnais 🌐

December 7, 2020

Abstract

This Isabelle/HOL formalization builds on the VeriComp entry of the Archive of Formal Proofs to provide the following contributions:
  • an operational semantics for a realistic virtual machine (Std) for dynamically typed programming languages;
  • the formalization of an inline caching optimization (Inca), a proof of bisimulation with (Std), and a compilation function;
  • the formalization of an unboxing optimization (Ubx), a proof of bisimulation with (Inca), and a simple compilation function.
This formalization was described in the CPP 2021 paper Towards Efficient and Verified Virtual Machines for Dynamic Languages
BSD License

Change history

June 25, 2021

proved conditional completeness of compilation

June 14, 2021

refactored function definitions to contain explicit basic blocks
-

Topics

Theories of Interpreter_Optimizations

Depends On

Cite

× 
@article{Interpreter_Optimizations-AFP,
   author  = {Martin Desharnais},
   title   = {Inline Caching and Unboxing Optimization for Interpreters},
   journal = {Archive of Formal Proofs},
   month   = {December},
   year    = {2020},
   note    = {\url{https://isa-afp.org/entries/Interpreter_Optimizations.html},
             Formal proof development},
   ISSN    = {2150-914x},
 }
Download

Download

× Download latest

Older releases:

\ No newline at end of file diff --git a/web/entries/Jordan_Normal_Form.html b/web/entries/Jordan_Normal_Form.html --- a/web/entries/Jordan_Normal_Form.html +++ b/web/entries/Jordan_Normal_Form.html @@ -1,237 +1,236 @@ Matrices, Jordan Normal Forms, and Spectral Radius Theory - Archive of Formal Proofs

Matrices, Jordan Normal Forms, and Spectral Radius Theory

René Thiemann 📧 and Akihisa Yamada 📧 with contributions from Alexander Bentkamp 📧

August 21, 2015

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.

BSD License

Change history

April 17, 2018

Integrated lemmas from deep-learning AFP-entry of Alexander Bentkamp

January 7, 2016

Added Schur-decomposition, Gram-Schmidt orthogonalization, uniqueness of Jordan normal forms
-

Topics

Theories of Jordan_Normal_Form

Depends On

Used by

Related Entries

Cite

× 
@article{Jordan_Normal_Form-AFP,
   author  = {René Thiemann and Akihisa Yamada},
   title   = {Matrices, Jordan Normal Forms, and Spectral Radius Theory},
   journal = {Archive of Formal Proofs},
   month   = {August},
   year    = {2015},
   note    = {\url{https://isa-afp.org/entries/Jordan_Normal_Form.html},
             Formal proof development},
   ISSN    = {2150-914x},
 }
Download

Download

× Download latest

Older releases:

\ No newline at end of file diff --git a/web/entries/LLL_Basis_Reduction.html b/web/entries/LLL_Basis_Reduction.html --- a/web/entries/LLL_Basis_Reduction.html +++ b/web/entries/LLL_Basis_Reduction.html @@ -1,208 +1,207 @@ A verified LLL algorithm - Archive of Formal Proofs

A Verified LLL Algorithm

Ralph Bottesch, Jose Divasón 🌐, Max W. Haslbeck 🌐, Sebastiaan J. C. Joosten 🌐, René Thiemann 🌐 and Akihisa Yamada

February 2, 2018

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.
BSD License

Change history

May 25, 2018

Integrated much faster LLL implementation based on integer arithmetic (Bottesch, Haslbeck, Thiemann)

April 16, 2018

Integrated formal complexity bounds (Haslbeck, Thiemann) -

Topics

Theories of LLL_Basis_Reduction

Depends On

Used by

Cite

× 
@article{LLL_Basis_Reduction-AFP,
   author  = {Ralph Bottesch and Jose Divasón and Max W. Haslbeck and Sebastiaan J. C. Joosten and René Thiemann and Akihisa Yamada},
   title   = {A verified LLL algorithm},
   journal = {Archive of Formal Proofs},
   month   = {February},
   year    = {2018},
   note    = {\url{https://isa-afp.org/entries/LLL_Basis_Reduction.html},
             Formal proof development},
   ISSN    = {2150-914x},
 }
Download

Download

× Download latest

Older releases:

\ No newline at end of file diff --git a/web/entries/LTL_to_DRA.html b/web/entries/LTL_to_DRA.html --- a/web/entries/LTL_to_DRA.html +++ b/web/entries/LTL_to_DRA.html @@ -1,201 +1,200 @@ Converting Linear Temporal Logic to Deterministic (Generalized) Rabin Automata - Archive of Formal Proofs

Converting Linear Temporal Logic to Deterministic (Generalized) Rabin Automata

Salomon Sickert 📧

September 4, 2015

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.
BSD License

Change history

March 24, 2016

Make use of the LTL entry and include the simplifier.

September 23, 2015

Enable code export for the eager unfolding optimisation and reduce running time of the generated tool. Moreover, add support for the mlton SML compiler.
-

Topics

Theories of LTL_to_DRA

Depends On

Cite

× 
@article{LTL_to_DRA-AFP,
   author  = {Salomon Sickert},
   title   = {Converting Linear Temporal Logic to Deterministic (Generalized) Rabin Automata},
   journal = {Archive of Formal Proofs},
   month   = {September},
   year    = {2015},
   note    = {\url{https://isa-afp.org/entries/LTL_to_DRA.html},
             Formal proof development},
   ISSN    = {2150-914x},
 }
Download

Download

× Download latest

Older releases:

\ No newline at end of file diff --git a/web/entries/Launchbury.html b/web/entries/Launchbury.html --- a/web/entries/Launchbury.html +++ b/web/entries/Launchbury.html @@ -1,250 +1,249 @@ The Correctness of Launchbury's Natural Semantics for Lazy Evaluation - Archive of Formal Proofs

The Correctness of Launchbury's Natural Semantics for Lazy Evaluation

Joachim Breitner 🌐

January 31, 2013

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.
BSD License

Change history

March 16, 2015

Booleans and if-then-else added to syntax and semantics, making this entry suitable to be used by the entry "Call_Arity".

May 24, 2014

Added the proof of adequacy, as well as simplified and improved the existing proofs. Adjusted abstract accordingly. -

Topics

Theories of Launchbury

Depends On

Used by

Related Entries

Cite

× 
@article{Launchbury-AFP,
   author  = {Joachim Breitner},
   title   = {The Correctness of Launchbury's Natural Semantics for Lazy Evaluation},
   journal = {Archive of Formal Proofs},
   month   = {January},
   year    = {2013},
   note    = {\url{https://isa-afp.org/entries/Launchbury.html},
             Formal proof development},
   ISSN    = {2150-914x},
 }
Download

Download

× Download latest

Older releases:

\ No newline at end of file diff --git a/web/entries/Native_Word.html b/web/entries/Native_Word.html --- a/web/entries/Native_Word.html +++ b/web/entries/Native_Word.html @@ -1,249 +1,248 @@ Native Word - Archive of Formal Proofs

Native Word

Andreas Lochbihler 🌐 with contributions from Peter Lammich 🌐

September 17, 2013

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.
BSD License

Change history

July 15, 2018

added cast operators for default-size words (revision fc1f1fb8dd30)

September 2, 2017

added 64-bit words (revision c89f86244e3c)
-

October 6, 2014

proper test setup with compilation and execution of tests in all target languages (revision 5d7a1c9ae047)

March 31, 2014

added words of default size in the target language (by Peter Lammich) (revision 25caf5065833)

November 6, 2013

added conversion function between native words and characters (revision fd23d9a7fe3a)

Topics

Theories of Native_Word

Depends On

Used by

Related Entries

Cite

× 
@article{Native_Word-AFP,
   author  = {Andreas Lochbihler},
   title   = {Native Word},
   journal = {Archive of Formal Proofs},
   month   = {September},
   year    = {2013},
   note    = {\url{https://isa-afp.org/entries/Native_Word.html},
             Formal proof development},
   ISSN    = {2150-914x},
 }
Download

Download

× Download latest

Older releases:

\ No newline at end of file diff --git a/web/entries/Ordinary_Differential_Equations.html b/web/entries/Ordinary_Differential_Equations.html --- a/web/entries/Ordinary_Differential_Equations.html +++ b/web/entries/Ordinary_Differential_Equations.html @@ -1,306 +1,303 @@ Ordinary Differential Equations - Archive of Formal Proofs

Ordinary Differential Equations

Fabian Immler 🌐 and Johannes Hölzl 🌐

April 26, 2012

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:

  • HOL-ODE-Numerics: Rigorous numerical algorithms for computing enclosures of solutions based on Runge-Kutta methods and affine arithmetic. Reachability analysis with splitting and reduction at hyperplanes.
  • HOL-ODE-Examples: Applications of the numerical algorithms to concrete systems of ODEs.
  • Lorenz_C0, Lorenz_C1: Verified algorithms for checking C1-information according to Tucker's proof, computation of C0-information.

BSD License

Change history

September 20, 2017

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.

August 3, 2016

numerical algorithms for reachability analysis (using second-order Runge-Kutta methods, splitting, and reduction) implemented using Lammich's framework for automatic refinement
-

April 14, 2016

added flow and variational equation
-

February 13, 2014

added an implementation of the Euler method based on affine arithmetic
-

Topics

Theories of Ordinary_Differential_Equations

Theories of HOL-ODE-Numerics

Theories of Lorenz_Approximation

Theories of HOL-ODE-Examples

Theories of HOL-ODE-ARCH-COMP

Theories of Lorenz_C0

Theories of Lorenz_C1

Depends On

Used by

Related Entries

Cite

× 
@article{Ordinary_Differential_Equations-AFP,
   author  = {Fabian Immler and Johannes Hölzl},
   title   = {Ordinary Differential Equations},
   journal = {Archive of Formal Proofs},
   month   = {April},
   year    = {2012},
   note    = {\url{https://isa-afp.org/entries/Ordinary_Differential_Equations.html},
             Formal proof development},
   ISSN    = {2150-914x},
 }
Download

Download

× Download latest

Older releases:

\ 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,251 +1,249 @@ Executable Multivariate Polynomials - Archive of Formal Proofs

Executable Multivariate Polynomials

Christian Sternagel 📧, René Thiemann 🌐, Alexander Maletzky 🌐, Fabian Immler 🌐, Florian Haftmann 🌐, Andreas Lochbihler 🌐 and Alexander Bentkamp 📧

August 10, 2010

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].

GNU Lesser General Public License (LGPL)

Change history

April 18, 2019

Added material about polynomials whose power-products are represented themselves by polynomial mappings.

January 23, 2018

Added authors Haftmann, Lochbihler after incorporating their formalization of multivariate polynomials based on Polynomial mappings. Moved material from Bentkamp's entry "Deep Learning".

October 28, 2016

Added abstract representation of polynomials and authors Maletzky/Immler.
-

September 17, 2010

Moved theories on arbitrary (ordered) semirings to Abstract Rewriting.
-

Topics

Theories of Polynomials

Depends On

Used by

Cite

× 
@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   = {August},
   year    = {2010},
   note    = {\url{https://isa-afp.org/entries/Polynomials.html},
             Formal proof development},
   ISSN    = {2150-914x},
 }
Download

Download

× Download latest

Older releases:

\ No newline at end of file diff --git a/web/entries/Regular-Sets.html b/web/entries/Regular-Sets.html --- a/web/entries/Regular-Sets.html +++ b/web/entries/Regular-Sets.html @@ -1,211 +1,210 @@ Regular Sets and Expressions - Archive of Formal Proofs

Regular Sets and Expressions

Alexander Krauss 🌐 and Tobias Nipkow 🌐 with contributions from Manuel Eberl 🌐

May 12, 2010

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.

BSD License

Change history

May 10, 2012

Tobias Nipkow added equivalence checking with partial derivatives

August 26, 2011

Christian Urban added a theory about derivatives and partial derivatives of regular expressions
-

Topics

Theories of Regular-Sets

Used by

Cite

× 
@article{Regular-Sets-AFP,
   author  = {Alexander Krauss and Tobias Nipkow},
   title   = {Regular Sets and Expressions},
   journal = {Archive of Formal Proofs},
   month   = {May},
   year    = {2010},
   note    = {\url{https://isa-afp.org/entries/Regular-Sets.html},
             Formal proof development},
   ISSN    = {2150-914x},
 }
Download

Download

× Download latest

Older releases:

\ No newline at end of file diff --git a/web/entries/Resolution_FOL.html b/web/entries/Resolution_FOL.html --- a/web/entries/Resolution_FOL.html +++ b/web/entries/Resolution_FOL.html @@ -1,218 +1,218 @@ The Resolution Calculus for First-Order Logic - Archive of Formal Proofs

The Resolution Calculus for First-Order Logic

Anders Schlichtkrull 🌐

June 30, 2016

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.

BSD License

Change history

March 20, 2018

- added a concrete instance of the unification and completeness theorems using the First-Order Terms AFP-entry from IsaFoR as described in the papers + added a concrete instance of the unification and completeness theorems using the First-Order Terms AFP-entry from IsaFoR as described in the papers

January 24, 2018

- added several new versions of the soundness and completeness theorems as described in the paper + added several new versions of the soundness and completeness theorems as described in the paper

Topics

Theories of Resolution_FOL

Depends On

Cite

× 
@article{Resolution_FOL-AFP,
   author  = {Anders Schlichtkrull},
   title   = {The Resolution Calculus for First-Order Logic},
   journal = {Archive of Formal Proofs},
   month   = {June},
   year    = {2016},
   note    = {\url{https://isa-afp.org/entries/Resolution_FOL.html},
             Formal proof development},
   ISSN    = {2150-914x},
 }
Download

Download

× Download latest

Older releases:

\ 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,216 +1,215 @@ Haskell's Show Class in Isabelle/HOL - Archive of Formal Proofs

Haskell's Show Class in Isabelle/HOL

Christian Sternagel 📧 and René Thiemann 📧

July 29, 2014

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".
GNU Lesser General Public License (LGPL)

Change history

April 10, 2015

Moved development for old-style datatypes into subdirectory "Old_Datatype".

March 11, 2015

Adapted development to new-style (BNF-based) datatypes.
-

Topics

Theories of Show

Theories of Old_Datatype_Show

Depends On

Used by

Related Entries

Cite

× 
@article{Show-AFP,
   author  = {Christian Sternagel and René Thiemann},
   title   = {Haskell's Show Class in Isabelle/HOL},
   journal = {Archive of Formal Proofs},
   month   = {July},
   year    = {2014},
   note    = {\url{https://isa-afp.org/entries/Show.html},
             Formal proof development},
   ISSN    = {2150-914x},
 }
Download

Download

× Download latest

Older releases:

\ No newline at end of file diff --git a/web/entries/Sqrt_Babylonian.html b/web/entries/Sqrt_Babylonian.html --- a/web/entries/Sqrt_Babylonian.html +++ b/web/entries/Sqrt_Babylonian.html @@ -1,203 +1,202 @@ Computing N-th Roots using the Babylonian Method - Archive of Formal Proofs

Computing N-Th Roots Using the Babylonian Method

René Thiemann 📧

January 3, 2013

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.
GNU Lesser General Public License (LGPL)

Change history

July 11, 2014

Moved NthRoot_Impl from Real-Impl to this entry.

October 16, 2013

Added algorithms to compute floor and ceiling of sqrt of integers. -

Topics

Theories of Sqrt_Babylonian

Depends On

Used by

Cite

× 
@article{Sqrt_Babylonian-AFP,
   author  = {René Thiemann},
   title   = {Computing N-th Roots using the Babylonian Method},
   journal = {Archive of Formal Proofs},
   month   = {January},
   year    = {2013},
   note    = {\url{https://isa-afp.org/entries/Sqrt_Babylonian.html},
             Formal proof development},
   ISSN    = {2150-914x},
 }
Download

Download

× Download latest

Older releases:

\ 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,241 +1,238 @@ Well-Quasi-Orders - Archive of Formal Proofs

Well-Quasi-Orders

Christian Sternagel 📧

April 13, 2012

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.
BSD License

Change history

June 8, 2017

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.

January 3, 2016

An alternative proof of Higman's lemma by open induction.
-

July 9, 2014

Simplified proofs of Higman's lemma and Kruskal's tree theorem, based on homogeneous sequences.

May 16, 2013

Simplified construction of minimal bad sequences.
-

December 19, 2012

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.

June 11, 2012

Added Kruskal's Tree Theorem.
-

Topics

Theories of Well_Quasi_Orders

Depends On

Used by

Cite

× 
@article{Well_Quasi_Orders-AFP,
   author  = {Christian Sternagel},
   title   = {Well-Quasi-Orders},
   journal = {Archive of Formal Proofs},
   month   = {April},
   year    = {2012},
   note    = {\url{https://isa-afp.org/entries/Well_Quasi_Orders.html},
             Formal proof development},
   ISSN    = {2150-914x},
 }
Download

Download

× Download latest

Older releases:

\ No newline at end of file