diff --git a/web/entries/AODV.shtml b/web/entries/AODV.shtml --- a/web/entries/AODV.shtml +++ b/web/entries/AODV.shtml @@ -1,139 +1,143 @@ Archive of Formal Proofs

 

Loop freedom of the (untimed) AODV routing protocol

+ + + +
Title: Loop freedom of the (untimed) AODV routing protocol
Author: Timothy Bourke and Peter Höfner
Submission date: 2014-10-23
Abstract:

The Ad hoc On-demand Distance Vector (AODV) routing protocol allows the nodes in a Mobile Ad hoc Network (MANET) or a Wireless Mesh Network (WMN) to know where to forward data packets. Such a protocol is ‘loop free’ if it never leads to routing decisions that forward packets in circles.

This development mechanises an existing pen-and-paper proof of loop freedom of AODV. The protocol is modelled in the Algebra of Wireless Networks (AWN), which is the subject of an earlier paper and AFP mechanization. The proof relies on a novel compositional approach for lifting invariants to networks of nodes.

We exploit the mechanization to analyse several variants of AODV and show that Isabelle/HOL can re-establish most proof obligations automatically and identify exactly the steps that are no longer valid.

BibTeX: 
@article{AODV-AFP,
   author  = {Timothy Bourke and Peter Höfner},
   title   = {Loop freedom of the (untimed) AODV routing protocol},
   journal = {Archive of Formal Proofs},
   month   = oct,
   year    = 2014,
   note    = {\url{http://afp.sf.net/entries/AODV.shtml},
             Formal proof development},
   ISSN    = {2150-914x},
 }
License: BSD License
Depends on:AWN

">Proof outline
">Proof document
">Browse theories
">Download this entry
Older releases:
diff --git a/web/entries/Abstract-Rewriting.shtml b/web/entries/Abstract-Rewriting.shtml --- a/web/entries/Abstract-Rewriting.shtml +++ b/web/entries/Abstract-Rewriting.shtml @@ -1,142 +1,146 @@ Archive of Formal Proofs

 

Abstract Rewriting

+ + + +
Title: Abstract Rewriting
Author: Christian Sternagel 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://afp.sf.net/entries/Abstract-Rewriting.shtml},
             Formal proof development},
   ISSN    = {2150-914x},
 }
License: GNU Lesser General Public License (LGPL)
Depends on:Regular-Sets

">Proof outline
">Proof document
">Browse theories
">Download this entry
Older releases:
diff --git a/web/entries/Abstract_Completeness.shtml b/web/entries/Abstract_Completeness.shtml --- a/web/entries/Abstract_Completeness.shtml +++ b/web/entries/Abstract_Completeness.shtml @@ -1,117 +1,121 @@ Archive of Formal Proofs

 

Abstract Completeness

+ + + +
Title: Abstract Completeness
Author: Jasmin Christian Blanchette, Andrei Popescu and Dmitriy Traytel
Submission date: 2014-04-16
Abstract: A formalization of an abstract property of possibly infinite derivation trees (modeled by a codatatype), representing the core of a proof (in Beth/Hintikka style) of the first-order logic completeness theorem, independent of the concrete syntax or inference rules. This work is described in detail in the IJCAR 2014 publication by the authors. The abstract proof can be instantiated for a wide range of Gentzen and tableau systems as well as various flavors of FOL---e.g., with or without predicates, equality, or sorts. Here, we give only a toy example instantiation with classical propositional logic. A more serious instance---many-sorted FOL with equality---is described elsewhere [Blanchette and Popescu, FroCoS 2013].
BibTeX: 
@article{Abstract_Completeness-AFP,
   author  = {Jasmin Christian Blanchette and Andrei Popescu and Dmitriy Traytel},
   title   = {Abstract Completeness},
   journal = {Archive of Formal Proofs},
   month   = apr,
   year    = 2014,
   note    = {\url{http://afp.sf.net/entries/Abstract_Completeness.shtml},
             Formal proof development},
   ISSN    = {2150-914x},
 }
License: BSD License
Depends on:Collections

">Proof outline
">Proof document
">Browse theories
">Download this entry
Older releases:
diff --git a/web/entries/Algebraic_Numbers.shtml b/web/entries/Algebraic_Numbers.shtml --- a/web/entries/Algebraic_Numbers.shtml +++ b/web/entries/Algebraic_Numbers.shtml @@ -1,129 +1,129 @@ Archive of Formal Proofs

 

Algebraic Numbers in Isabelle/HOL

- +
Title: Algebraic Numbers in Isabelle/HOL
Author: René Thiemann (rene /dot/ thiemann /at/ uibk /dot/ ac /dot/ at) and Akihisa Yamada (akihisa /dot/ yamada /at/ uibk /dot/ ac /dot/ at)
Submission date: 2015-12-22
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.

Change history: [2016-01-29]: Split off Polynomial Interpolation and Polynomial Factorization
BibTeX: 
@article{Algebraic_Numbers-AFP,
   author  = {René Thiemann and Akihisa Yamada},
   title   = {Algebraic Numbers in Isabelle/HOL},
   journal = {Archive of Formal Proofs},
   month   = dec,
   year    = 2015,
   note    = {\url{http://afp.sf.net/entries/Algebraic_Numbers.shtml},
             Formal proof development},
   ISSN    = {2150-914x},
 }
License: BSD License
Depends on:Sturm_Sequences, Partial_Function_MR, Sqrt_Babylonian, Show, Jordan_Normal_Form, Deriving, Polynomial_Factorization
Sturm_Sequences, Show, Deriving, Polynomial_Interpolation, Abstract-Rewriting, Jordan_Normal_Form, Polynomial_Factorization, Containers

">Proof outline
">Proof document
">Browse theories
">Download this entry
Older releases:
diff --git a/web/entries/Amortized_Complexity.shtml b/web/entries/Amortized_Complexity.shtml --- a/web/entries/Amortized_Complexity.shtml +++ b/web/entries/Amortized_Complexity.shtml @@ -1,135 +1,135 @@ Archive of Formal Proofs

 

Amortized Complexity Verified

- +
Title: Amortized Complexity Verified
Author: Tobias Nipkow
Submission date: 2014-07-07
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. This work is described in a paper published in the proceedings of the conference on Interactive Theorem Proving ITP 2015.
Change history: [2015-03-17]: Added pairing heaps by Hauke Brinkop.
BibTeX: 
@article{Amortized_Complexity-AFP,
   author  = {Tobias Nipkow},
   title   = {Amortized Complexity Verified},
   journal = {Archive of Formal Proofs},
   month   = jul,
   year    = 2014,
   note    = {\url{http://afp.sf.net/entries/Amortized_Complexity.shtml},
             Formal proof development},
   ISSN    = {2150-914x},
 }
License: BSD License
Depends on:Splay_Tree, Skew_Heap
Splay_Tree, Skew_Heap, List-Index

">Proof outline
">Proof document
">Browse theories
">Download this entry
Older releases:
diff --git a/web/entries/AutoFocus-Stream.shtml b/web/entries/AutoFocus-Stream.shtml --- a/web/entries/AutoFocus-Stream.shtml +++ b/web/entries/AutoFocus-Stream.shtml @@ -1,128 +1,132 @@ Archive of Formal Proofs

 

AutoFocus Stream Processing for Single-Clocking and Multi-Clocking Semantics

+ + + +
Title: AutoFocus Stream Processing for Single-Clocking and Multi-Clocking Semantics
Author: David Trachtenherz
Submission date: 2011-02-23
Abstract: We formalize the AutoFocus Semantics (a time-synchronous subset of the Focus formalism) as stream processing functions on finite and infinite message streams represented as finite/infinite lists. The formalization comprises both the conventional single-clocking semantics (uniform global clock for all components and communications channels) and its extension to multi-clocking semantics (internal execution clocking of a component may be a multiple of the external communication clocking). The semantics is defined by generic stream processing functions making it suitable for simulation/code generation in Isabelle/HOL. Furthermore, a number of AutoFocus semantics properties are formalized using definitions from the IntervalLogic theories.
BibTeX: 
@article{AutoFocus-Stream-AFP,
   author  = {David Trachtenherz},
   title   = {AutoFocus Stream Processing for Single-Clocking and Multi-Clocking Semantics},
   journal = {Archive of Formal Proofs},
   month   = feb,
   year    = 2011,
   note    = {\url{http://afp.sf.net/entries/AutoFocus-Stream.shtml},
             Formal proof development},
   ISSN    = {2150-914x},
 }
License: BSD License
Depends on:List-Infinite, Nat-Interval-Logic

">Proof outline
">Proof document
">Browse theories
">Download this entry
Older releases:
diff --git a/web/entries/CAVA_Automata.shtml b/web/entries/CAVA_Automata.shtml --- a/web/entries/CAVA_Automata.shtml +++ b/web/entries/CAVA_Automata.shtml @@ -1,146 +1,146 @@ Archive of Formal Proofs

 

The CAVA Automata Library

- +
Title: The CAVA Automata Library
Author: Peter Lammich
Submission date: 2014-05-28
Abstract: We report on the graph and automata library that is used in the fully verified LTL model checker CAVA. As most components of CAVA use some type of graphs or automata, a common automata library simplifies assembly of the components and reduces redundancy.

The CAVA Automata Library provides a hierarchy of graph and automata classes, together with some standard algorithms. Its object oriented design allows for sharing of algorithms, theorems, and implementations between its classes, and also simplifies extensions of the library. Moreover, it is integrated into the Automatic Refinement Framework, supporting automatic refinement of the abstract automata types to efficient data structures.

Note that the CAVA Automata Library is work in progress. Currently, it is very specifically tailored towards the requirements of the CAVA model checker. Nevertheless, the formalization techniques presented here allow an extension of the library to a wider scope. Moreover, they are not limited to graph libraries, but apply to class hierarchies in general.

The CAVA Automata Library is described in the paper: Peter Lammich, The CAVA Automata Library, Isabelle Workshop 2014.

BibTeX: 
@article{CAVA_Automata-AFP,
   author  = {Peter Lammich},
   title   = {The CAVA Automata Library},
   journal = {Archive of Formal Proofs},
   month   = may,
   year    = 2014,
   note    = {\url{http://afp.sf.net/entries/CAVA_Automata.shtml},
             Formal proof development},
   ISSN    = {2150-914x},
 }
License: BSD License
Depends on:Collections
Collections, Native_Word

">Proof outline
">Proof document
">Browse theories
">Download this entry
Older releases:
diff --git a/web/entries/CAVA_LTL_Modelchecker.shtml b/web/entries/CAVA_LTL_Modelchecker.shtml --- a/web/entries/CAVA_LTL_Modelchecker.shtml +++ b/web/entries/CAVA_LTL_Modelchecker.shtml @@ -1,142 +1,142 @@ Archive of Formal Proofs

 

A Fully Verified Executable LTL Model Checker

- +
Title: A Fully Verified Executable LTL Model Checker
Author: Javier Esparza, Peter Lammich, René Neumann (rene /dot/ neumann /at/ in /dot/ tum /dot/ de), Tobias Nipkow, Alexander Schimpf (schimpfa /at/ informatik /dot/ uni-freiburg /dot/ de) and Jan-Georg Smaus
Submission date: 2014-05-28
Abstract: We present an LTL model checker whose code has been completely verified using the Isabelle theorem prover. The checker consists of over 4000 lines of ML code. The code is produced using the Isabelle Refinement Framework, which allows us to split its correctness proof into (1) the proof of an abstract version of the checker, consisting of a few hundred lines of ``formalized pseudocode'', and (2) a verified refinement step in which mathematical sets and other abstract structures are replaced by implementations of efficient structures like red-black trees and functional arrays. This leads to a checker that, while still slower than unverified checkers, can already be used as a trusted reference implementation against which advanced implementations can be tested.

An early version of this model checker is described in the CAV 2013 paper with the same title.

BibTeX: 
@article{CAVA_LTL_Modelchecker-AFP,
   author  = {Javier Esparza and Peter Lammich and René Neumann and Tobias Nipkow and Alexander Schimpf and Jan-Georg Smaus},
   title   = {A Fully Verified Executable LTL Model Checker},
   journal = {Archive of Formal Proofs},
   month   = may,
   year    = 2014,
   note    = {\url{http://afp.sf.net/entries/CAVA_LTL_Modelchecker.shtml},
             Formal proof development},
   ISSN    = {2150-914x},
 }
License: BSD License
Depends on:Gabow_SCC, Promela, LTL_to_GBA
CAVA_Automata, Gabow_SCC, Promela, LTL_to_GBA

">Proof outline
">Proof document
">Browse theories
">Download this entry
Older releases:
diff --git a/web/entries/Call_Arity.shtml b/web/entries/Call_Arity.shtml --- a/web/entries/Call_Arity.shtml +++ b/web/entries/Call_Arity.shtml @@ -1,144 +1,148 @@ Archive of Formal Proofs

 

The Safety of Call Arity

+ + + +
Title: The Safety of Call Arity
Author: Joachim Breitner
Submission date: 2015-02-20
Abstract: We formalize the Call Arity analysis, as implemented in GHC, and prove both functional correctness and, more interestingly, safety (i.e. the transformation does not increase allocation).

We use syntax and the denotational semantics from the entry "Launchbury", where we formalized Launchbury's natural semantics for lazy evaluation.

The functional correctness of Call Arity is proved with regard to that denotational semantics. The operational properties are shown with regard to a small-step semantics akin to Sestoft's mark 1 machine, which we prove to be equivalent to Launchbury's semantics.

We use Christian Urban's Nominal2 package to define our terms and make use of Brian Huffman's HOLCF package for the domain-theoretical aspects of the development.

Change history: [2015-03-16]: This entry now builds on top of the Launchbury entry, and the equivalency proof of the natural and the small-step semantics was added.
BibTeX: 
@article{Call_Arity-AFP,
   author  = {Joachim Breitner},
   title   = {The Safety of Call Arity},
   journal = {Archive of Formal Proofs},
   month   = feb,
   year    = 2015,
   note    = {\url{http://afp.sf.net/entries/Call_Arity.shtml},
             Formal proof development},
   ISSN    = {2150-914x},
 }
License: BSD License
Depends on:Launchbury

">Proof outline
">Proof document
">Browse theories
">Download this entry
Older releases:
diff --git a/web/entries/Certification_Monads.shtml b/web/entries/Certification_Monads.shtml --- a/web/entries/Certification_Monads.shtml +++ b/web/entries/Certification_Monads.shtml @@ -1,119 +1,119 @@ Archive of Formal Proofs

 

Certification Monads

- +
Title: Certification Monads
Author: Christian Sternagel (c /dot/ sternagel /at/ gmail /dot/ com) and René Thiemann (rene /dot/ thiemann /at/ uibk /dot/ ac /dot/ at)
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://afp.sf.net/entries/Certification_Monads.shtml},
             Formal proof development},
   ISSN    = {2150-914x},
 }
License: BSD License
Depends on:Show, Partial_Function_MR
Partial_Function_MR, Show

">Proof outline
">Proof document
">Browse theories
">Download this entry
Older releases:
diff --git a/web/entries/Coinductive_Languages.shtml b/web/entries/Coinductive_Languages.shtml --- a/web/entries/Coinductive_Languages.shtml +++ b/web/entries/Coinductive_Languages.shtml @@ -1,136 +1,140 @@ Archive of Formal Proofs

 

A Codatatype of Formal Languages

+ + + +
Title: A Codatatype of Formal Languages
Author: Dmitriy Traytel (traytel /at/ in /dot/ tum /dot/ de)
Submission date: 2013-11-15
Abstract:

We define formal languages as a codataype of infinite trees branching over the alphabet. Each node in such a tree indicates whether the path to this node constitutes a word inside or outside of the language. This codatatype is isormorphic to the set of lists representation of languages, but caters for definitions by corecursion and proofs by coinduction.

Regular operations on languages are then defined by primitive corecursion. A difficulty arises here, since the standard definitions of concatenation and iteration from the coalgebraic literature are not primitively corecursive-they require guardedness up-to union/concatenation. Without support for up-to corecursion, these operation must be defined as a composition of primitive ones (and proved being equal to the standard definitions). As an exercise in coinduction we also prove the axioms of Kleene algebra for the defined regular operations.

Furthermore, a language for context-free grammars given by productions in Greibach normal form and an initial nonterminal is constructed by primitive corecursion, yielding an executable decision procedure for the word problem without further ado.

BibTeX: 
@article{Coinductive_Languages-AFP,
   author  = {Dmitriy Traytel},
   title   = {A Codatatype of Formal Languages},
   journal = {Archive of Formal Proofs},
   month   = nov,
   year    = 2013,
   note    = {\url{http://afp.sf.net/entries/Coinductive_Languages.shtml},
             Formal proof development},
   ISSN    = {2150-914x},
 }
License: BSD License
Depends on:Regular-Sets

">Proof outline
">Proof document
">Browse theories
">Download this entry
Older releases:
diff --git a/web/entries/Collections.shtml b/web/entries/Collections.shtml --- a/web/entries/Collections.shtml +++ b/web/entries/Collections.shtml @@ -1,155 +1,155 @@ Archive of Formal Proofs

 

Collections Framework

- +
Title: Collections Framework
Author: Peter Lammich
Contributors: Andreas Lochbihler and Thomas Tuerk
Submission date: 2009-11-25
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.
Change 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.
[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-08]: Collections V2. New features: Polymorphic iterators. Generic algorithm instantiation where required. Naming scheme changed from xx_opname to xx.opname. A compatibility file CollectionsV1 tries to simplify porting of existing theories, by providing old naming scheme and the old monomorphic iterator locales.
[2013-09]: Added Generic Collection Framework based on Autoref. The GenCF provides: Arbitrary nesting, full integration with Autoref.
[2014-06]: Maintenace changes to GenCF: Optimized inj_image on list_set. op_set_cart (Cartesian product). big-Union operation. atLeastLessThan - operation ({a..<b})
BibTeX: 
@article{Collections-AFP,
   author  = {Peter Lammich},
   title   = {Collections Framework},
   journal = {Archive of Formal Proofs},
   month   = nov,
   year    = 2009,
   note    = {\url{http://afp.sf.net/entries/Collections.shtml},
             Formal proof development},
   ISSN    = {2150-914x},
 }
License: BSD License
Depends on:Binomial-Heaps, Finger-Trees, Refine_Monadic
Finger-Trees, Native_Word, Trie, Automatic_Refinement, Refine_Monadic, Binomial-Heaps

">Proof outline
">Proof document
">Browse theories
">Download this entry
Older releases:
diff --git a/web/entries/Consensus_Refined.shtml b/web/entries/Consensus_Refined.shtml --- a/web/entries/Consensus_Refined.shtml +++ b/web/entries/Consensus_Refined.shtml @@ -1,131 +1,135 @@ Archive of Formal Proofs

 

Consensus Refined

+ + + +
Title: Consensus Refined
Author: Ognjen Maric (omaric /at/ inf /dot/ ethz /dot/ ch) and Christoph Sprenger (sprenger /at/ inf /dot/ ethz /dot/ ch)
Submission date: 2015-03-18
Abstract: Algorithms for solving the consensus problem are fundamental to distributed computing. Despite their brevity, their ability to operate in concurrent, asynchronous and failure-prone environments comes at the cost of complex and subtle behaviors. Accordingly, understanding how they work and proving their correctness is a non-trivial endeavor where abstraction is immensely helpful. Moreover, research on consensus has yielded a large number of algorithms, many of which appear to share common algorithmic ideas. A natural question is whether and how these similarities can be distilled and described in a precise, unified way. In this work, we combine stepwise refinement and lockstep models to provide an abstract and unified view of a sizeable family of consensus algorithms. Our models provide insights into the design choices underlying the different algorithms, and classify them based on those choices.
BibTeX: 
@article{Consensus_Refined-AFP,
   author  = {Ognjen Maric and Christoph Sprenger},
   title   = {Consensus Refined},
   journal = {Archive of Formal Proofs},
   month   = mar,
   year    = 2015,
   note    = {\url{http://afp.sf.net/entries/Consensus_Refined.shtml},
             Formal proof development},
   ISSN    = {2150-914x},
 }
License: BSD License
Depends on:Heard_Of, Stuttering_Equivalence

">Proof outline
">Proof document
">Browse theories
">Download this entry
Older releases:
diff --git a/web/entries/Containers.shtml b/web/entries/Containers.shtml --- a/web/entries/Containers.shtml +++ b/web/entries/Containers.shtml @@ -1,142 +1,142 @@ Archive of Formal Proofs

 

Light-weight Containers

- +
Title: Light-weight Containers
Author: Andreas Lochbihler
Contributors: René Thiemann (rene /dot/ thiemann /at/ uibk /dot/ ac /dot/ at)
Submission date: 2013-04-15
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.

Change history: [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)
BibTeX: 
@article{Containers-AFP,
   author  = {Andreas Lochbihler},
   title   = {Light-weight Containers},
   journal = {Archive of Formal Proofs},
   month   = apr,
   year    = 2013,
   note    = {\url{http://afp.sf.net/entries/Containers.shtml},
             Formal proof development},
   ISSN    = {2150-914x},
 }
License: BSD License
Depends on:Deriving
Deriving, Collections, Regular-Sets

">Proof outline
">Proof document
">Browse theories
">Download this entry
Older releases:
diff --git a/web/entries/Datatype_Order_Generator.shtml b/web/entries/Datatype_Order_Generator.shtml --- a/web/entries/Datatype_Order_Generator.shtml +++ b/web/entries/Datatype_Order_Generator.shtml @@ -1,140 +1,140 @@ Archive of Formal Proofs

 

Generating linear orders for datatypes

- +
Title: Generating linear orders for datatypes
Author: René Thiemann (rene /dot/ thiemann /at/ uibk /dot/ ac /dot/ at)
Submission date: 2012-08-07
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 (linear) orders or hash-functions which are required in the Isabelle Collection Framework. Moreover, for the tactic of Huffman and Krauss to show that a datatype is countable, we implemented a wrapper so that this tactic becomes accessible in our framework.

Our formalization was performed as part of the IsaFoR/CeTA project. With our new tactic we could completely remove tedious proofs for linear orders of two datatypes.

This development is aimed at datatypes generated by the "old_datatype" command.

BibTeX: 
@article{Datatype_Order_Generator-AFP,
   author  = {René Thiemann},
   title   = {Generating linear orders for datatypes},
   journal = {Archive of Formal Proofs},
   month   = aug,
   year    = 2012,
   note    = {\url{http://afp.sf.net/entries/Datatype_Order_Generator.shtml},
             Formal proof development},
   ISSN    = {2150-914x},
 }
License: BSD License
Depends on:Collections, Deriving
Deriving, Collections

">Proof outline
">Proof document
">Browse theories
">Download this entry
Older releases:
diff --git a/web/entries/Decreasing-Diagrams-II.shtml b/web/entries/Decreasing-Diagrams-II.shtml --- a/web/entries/Decreasing-Diagrams-II.shtml +++ b/web/entries/Decreasing-Diagrams-II.shtml @@ -1,119 +1,119 @@ Archive of Formal Proofs

 

Decreasing Diagrams II

- +
Title: Decreasing Diagrams II
Author: Bertram Felgenhauer (bertram /dot/ felgenhauer /at/ uibk /dot/ ac /dot/ at)
Submission date: 2015-08-20
Abstract: This theory formalizes the commutation version of decreasing diagrams for Church-Rosser modulo. The proof follows Felgenhauer and van Oostrom (RTA 2013). The theory also provides important specializations, in particular van Oostrom’s conversion version (TCS 2008) of decreasing diagrams.
BibTeX: 
@article{Decreasing-Diagrams-II-AFP,
   author  = {Bertram Felgenhauer},
   title   = {Decreasing Diagrams II},
   journal = {Archive of Formal Proofs},
   month   = aug,
   year    = 2015,
   note    = {\url{http://afp.sf.net/entries/Decreasing-Diagrams-II.shtml},
             Formal proof development},
   ISSN    = {2150-914x},
 }
License: GNU Lesser General Public License (LGPL)
Depends on:Abstract-Rewriting
Well_Quasi_Orders, Abstract-Rewriting

">Proof outline
">Proof document
">Browse theories
">Download this entry
Older releases:
diff --git a/web/entries/Descartes_Sign_Rule.shtml b/web/entries/Descartes_Sign_Rule.shtml --- a/web/entries/Descartes_Sign_Rule.shtml +++ b/web/entries/Descartes_Sign_Rule.shtml @@ -1,127 +1,123 @@ Archive of Formal Proofs

 

Descartes' Rule of Signs

- - - -
Title: Descartes' Rule of Signs
Author: Manuel Eberl
Submission date: 2015-12-28
Abstract: Descartes' Rule of Signs relates the number of positive real roots of a polynomial with the number of sign changes in its coefficient sequence. Our proof follows the simple inductive proof given by Rob Arthan, which was also used by John Harrison in his HOL Light formalisation. We proved most of the lemmas for arbitrary linearly-ordered integrity domains (e.g. integers, rationals, reals); the main result, however, requires the intermediate value theorem and was therefore only proven for real polynomials.
BibTeX: 
@article{Descartes_Sign_Rule-AFP,
   author  = {Manuel Eberl},
   title   = {Descartes' Rule of Signs},
   journal = {Archive of Formal Proofs},
   month   = dec,
   year    = 2015,
   note    = {\url{http://afp.sf.net/entries/Descartes_Sign_Rule.shtml},
             Formal proof development},
   ISSN    = {2150-914x},
 }
License: BSD License
Depends on:Sturm_Tarski

">Proof outline
">Proof document
">Browse theories
">Download this entry
Older releases:
diff --git a/web/entries/Dijkstra_Shortest_Path.shtml b/web/entries/Dijkstra_Shortest_Path.shtml --- a/web/entries/Dijkstra_Shortest_Path.shtml +++ b/web/entries/Dijkstra_Shortest_Path.shtml @@ -1,132 +1,132 @@ Archive of Formal Proofs

 

Dijkstra's Shortest Path Algorithm

- +
Title: Dijkstra's Shortest Path Algorithm
Author: Benedikt Nordhoff (b /dot/ n /at/ wwu /dot/ de) and Peter Lammich
Submission date: 2012-01-30
Abstract: We implement and prove correct Dijkstra's algorithm for the single source shortest path problem, conceived in 1956 by E. Dijkstra. The algorithm is implemented using the data refinement framework for monadic, nondeterministic programs. An efficient implementation is derived using data structures from the Isabelle Collection Framework.
BibTeX: 
@article{Dijkstra_Shortest_Path-AFP,
   author  = {Benedikt Nordhoff and Peter Lammich},
   title   = {Dijkstra's Shortest Path Algorithm},
   journal = {Archive of Formal Proofs},
   month   = jan,
   year    = 2012,
   note    = {\url{http://afp.sf.net/entries/Dijkstra_Shortest_Path.shtml},
             Formal proof development},
   ISSN    = {2150-914x},
 }
License: BSD License
Depends on:Refine_Monadic, Collections
Collections

">Proof outline
">Proof document
">Browse theories
">Download this entry
Older releases:
diff --git a/web/entries/Echelon_Form.shtml b/web/entries/Echelon_Form.shtml --- a/web/entries/Echelon_Form.shtml +++ b/web/entries/Echelon_Form.shtml @@ -1,115 +1,119 @@ Archive of Formal Proofs

 

Echelon Form

+ + + +
Title: Echelon Form
Author: Jose Divasón and Jesús Aransay
Submission date: 2015-02-12
Abstract: We formalize an algorithm to compute the Echelon Form of a matrix. We have proved its existence over Bézout domains and made it executable over Euclidean domains, such as the integer ring and the univariate polynomials over a field. This allows us to compute determinants, inverses and characteristic polynomials of matrices. The work is based on the HOL-Multivariate Analysis library, and on both the Gauss-Jordan and Cayley-Hamilton AFP entries. As a by-product, some algebraic structures have been implemented (principal ideal domains, Bézout domains...). The algorithm has been refined to immutable arrays and code can be generated to functional languages as well.
BibTeX: 
@article{Echelon_Form-AFP,
   author  = {Jose Divasón and Jesús Aransay},
   title   = {Echelon Form},
   journal = {Archive of Formal Proofs},
   month   = feb,
   year    = 2015,
   note    = {\url{http://afp.sf.net/entries/Echelon_Form.shtml},
             Formal proof development},
   ISSN    = {2150-914x},
 }
License: BSD License
Depends on:Gauss_Jordan, Cayley_Hamilton

">Proof outline
">Proof document
">Browse theories
">Download this entry
Older releases:
diff --git a/web/entries/Euler_Partition.shtml b/web/entries/Euler_Partition.shtml --- a/web/entries/Euler_Partition.shtml +++ b/web/entries/Euler_Partition.shtml @@ -1,119 +1,123 @@ Archive of Formal Proofs

 

Euler's Partition Theorem

+ + + +
Title: Euler's Partition Theorem
Author: Lukas Bulwahn (lukas /dot/ bulwahn /at/ gmail /dot/ com)
Submission date: 2015-11-19
Abstract: Euler's Partition Theorem states that the number of partitions with only distinct parts is equal to the number of partitions with only odd parts. The combinatorial proof follows John Harrison's HOL Light formalization. This theorem is the 45th theorem of the Top 100 Theorems list.
BibTeX: 
@article{Euler_Partition-AFP,
   author  = {Lukas Bulwahn},
   title   = {Euler's Partition Theorem},
   journal = {Archive of Formal Proofs},
   month   = nov,
   year    = 2015,
   note    = {\url{http://afp.sf.net/entries/Euler_Partition.shtml},
             Formal proof development},
   ISSN    = {2150-914x},
 }
License: BSD License
Depends on:Card_Number_Partitions

">Proof outline
">Proof document
">Browse theories
">Download this entry
Older releases:
diff --git a/web/entries/Finite_Automata_HF.shtml b/web/entries/Finite_Automata_HF.shtml --- a/web/entries/Finite_Automata_HF.shtml +++ b/web/entries/Finite_Automata_HF.shtml @@ -1,128 +1,128 @@ Archive of Formal Proofs

 

Finite Automata in Hereditarily Finite Set Theory

- +
Title: Finite Automata in Hereditarily Finite Set Theory
Author: Lawrence C. Paulson
Submission date: 2015-02-05
Abstract: Finite Automata, both deterministic and non-deterministic, for regular languages. The Myhill-Nerode Theorem. Closure under intersection, concatenation, etc. Regular expressions define regular languages. Closure under reversal; the powerset construction mapping NFAs to DFAs. Left and right languages; minimal DFAs. Brzozowski's minimization algorithm. Uniqueness up to isomorphism of minimal DFAs.
BibTeX: 
@article{Finite_Automata_HF-AFP,
   author  = {Lawrence C. Paulson},
   title   = {Finite Automata in Hereditarily Finite Set Theory},
   journal = {Archive of Formal Proofs},
   month   = feb,
   year    = 2015,
   note    = {\url{http://afp.sf.net/entries/Finite_Automata_HF.shtml},
             Formal proof development},
   ISSN    = {2150-914x},
 }
License: BSD License
Depends on:HereditarilyFinite
Regular-Sets, HereditarilyFinite

">Proof outline
">Proof document
">Browse theories
">Download this entry
Older releases:
diff --git a/web/entries/Flyspeck-Tame.shtml b/web/entries/Flyspeck-Tame.shtml --- a/web/entries/Flyspeck-Tame.shtml +++ b/web/entries/Flyspeck-Tame.shtml @@ -1,144 +1,148 @@ Archive of Formal Proofs

 

Flyspeck I: Tame Graphs

+ + + +
Title: Flyspeck I: Tame Graphs
Author: Gertrud Bauer and Tobias Nipkow
Submission date: 2006-05-22
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.
Change history: [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.
BibTeX: 
@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{http://afp.sf.net/entries/Flyspeck-Tame.shtml},
             Formal proof development},
   ISSN    = {2150-914x},
 }
License: BSD License
Depends on:Trie

">Proof outline
">Proof document
">Browse theories
">Download this entry
Older releases:
diff --git a/web/entries/Formal_SSA.shtml b/web/entries/Formal_SSA.shtml --- a/web/entries/Formal_SSA.shtml +++ b/web/entries/Formal_SSA.shtml @@ -1,139 +1,139 @@ Archive of Formal Proofs

 

Verified Construction of Static Single Assignment Form

- +
Title: Verified Construction of Static Single Assignment Form
Author: Sebastian Ullrich (sebasti /at/ nullri /dot/ ch) and Denis Lohner
Submission date: 2016-02-05
Abstract: We define a functional variant of the static single assignment (SSA) form construction algorithm described by Braun et al., which combines simplicity and efficiency. The definition is based on a general, abstract control flow graph representation using Isabelle locales.

We prove that the algorithm's output is semantically equivalent to the input according to a small-step semantics, and that it is in minimal SSA form for the common special case of reducible inputs. We then show the satisfiability of the locale assumptions by giving instantiations for a simple While language.

Furthermore, we use a generic instantiation based on typedefs in order to extract OCaml code and replace the unverified SSA construction algorithm of the CompCertSSA project with it.

BibTeX: 
@article{Formal_SSA-AFP,
   author  = {Sebastian Ullrich and Denis Lohner},
   title   = {Verified Construction of Static Single Assignment Form},
   journal = {Archive of Formal Proofs},
   month   = feb,
   year    = 2016,
   note    = {\url{http://afp.sf.net/entries/Formal_SSA.shtml},
             Formal proof development},
   ISSN    = {2150-914x},
 }
License: BSD License
Depends on:Slicing, Dijkstra_Shortest_Path
Slicing, Collections, Dijkstra_Shortest_Path

">Proof outline
">Proof document
">Browse theories
">Download this entry
Older releases:
diff --git a/web/entries/Formula_Derivatives.shtml b/web/entries/Formula_Derivatives.shtml --- a/web/entries/Formula_Derivatives.shtml +++ b/web/entries/Formula_Derivatives.shtml @@ -1,135 +1,135 @@ Archive of Formal Proofs

 

Derivatives of Logical Formulas

- +
Title: Derivatives of Logical Formulas
Author: Dmitriy Traytel
Submission date: 2015-05-28
Abstract: We formalize new decision procedures for WS1S, M2L(Str), and Presburger Arithmetics. Formulas of these logics denote regular languages. Unlike traditional decision procedures, we do not translate formulas into automata (nor into regular expressions), at least not explicitly. Instead we devise notions of derivatives (inspired by Brzozowski derivatives for regular expressions) that operate on formulas directly and compute a syntactic bisimulation using these derivatives. The treatment of Boolean connectives and quantifiers is uniform for all mentioned logics and is abstracted into a locale. This locale is then instantiated by different atomic formulas and their derivatives (which may differ even for the same logic under different encodings of interpretations as formal words).

The WS1S instance is described in the draft paper A Coalgebraic Decision Procedure for WS1S by the author.

BibTeX: 
@article{Formula_Derivatives-AFP,
   author  = {Dmitriy Traytel},
   title   = {Derivatives of Logical Formulas},
   journal = {Archive of Formal Proofs},
   month   = may,
   year    = 2015,
   note    = {\url{http://afp.sf.net/entries/Formula_Derivatives.shtml},
             Formal proof development},
   ISSN    = {2150-914x},
 }
License: BSD License
Depends on:Coinductive_Languages, Deriving, Show, List-Index
Deriving, Coinductive_Languages, List-Index, Show

">Proof outline
">Proof document
">Browse theories
">Download this entry
Older releases:
diff --git a/web/entries/Free-Groups.shtml b/web/entries/Free-Groups.shtml --- a/web/entries/Free-Groups.shtml +++ b/web/entries/Free-Groups.shtml @@ -1,138 +1,134 @@ Archive of Formal Proofs

 

Free Groups

- - - -
Title: Free Groups
Author: Joachim Breitner (mail /at/ joachim-breitner /dot/ de)
Submission date: 2010-06-24
Abstract: Free Groups are, in a sense, the most generic kind of group. They are defined over a set of generators with no additional relations in between them. They play an important role in the definition of group presentations and in other fields. This theory provides the definition of Free Group as the set of fully canceled words in the generators. The universal property is proven, as well as some isomorphisms results about Free Groups.
Change history: [2011-12-11]: Added the Ping Pong Lemma.
BibTeX: 
@article{Free-Groups-AFP,
   author  = {Joachim Breitner},
   title   = {Free Groups},
   journal = {Archive of Formal Proofs},
   month   = jun,
   year    = 2010,
   note    = {\url{http://afp.sf.net/entries/Free-Groups.shtml},
             Formal proof development},
   ISSN    = {2150-914x},
 }
License: BSD License
Depends on:Ordinals_and_Cardinals

">Proof outline
">Proof document
">Browse theories
">Download this entry
Older releases:
diff --git a/web/entries/Gauss_Jordan.shtml b/web/entries/Gauss_Jordan.shtml --- a/web/entries/Gauss_Jordan.shtml +++ b/web/entries/Gauss_Jordan.shtml @@ -1,118 +1,122 @@ Archive of Formal Proofs

 

Gauss-Jordan Algorithm and Its Applications

+ + + +
Title: Gauss-Jordan Algorithm and Its Applications
Author: Jose Divasón and Jesús Aransay
Submission date: 2014-09-03
Abstract: The Gauss-Jordan algorithm states that any matrix over a field can be transformed by means of elementary row operations to a matrix in reduced row echelon form. The formalization is based on the Rank Nullity Theorem entry of the AFP and on the HOL-Multivariate-Analysis session of Isabelle, where matrices are represented as functions over finite types. We have set up the code generator to make this representation executable. In order to improve the performance, a refinement to immutable arrays has been carried out. We have formalized some of the applications of the Gauss-Jordan algorithm. Thanks to this development, the following facts can be computed over matrices whose elements belong to a field: Ranks, Determinants, Inverses, Bases and dimensions and Solutions of systems of linear equations. Code can be exported to SML and Haskell.
BibTeX: 
@article{Gauss_Jordan-AFP,
   author  = {Jose Divasón and Jesús Aransay},
   title   = {Gauss-Jordan Algorithm and Its Applications},
   journal = {Archive of Formal Proofs},
   month   = sep,
   year    = 2014,
   note    = {\url{http://afp.sf.net/entries/Gauss_Jordan.shtml},
             Formal proof development},
   ISSN    = {2150-914x},
 }
License: BSD License
Depends on:Rank_Nullity_Theorem

">Proof outline
">Proof document
">Browse theories
">Download this entry
Older releases:
diff --git a/web/entries/Heard_Of.shtml b/web/entries/Heard_Of.shtml --- a/web/entries/Heard_Of.shtml +++ b/web/entries/Heard_Of.shtml @@ -1,151 +1,155 @@ Archive of Formal Proofs

 

Verifying Fault-Tolerant Distributed Algorithms in the Heard-Of Model

+ + + +
Title: Verifying Fault-Tolerant Distributed Algorithms in the Heard-Of Model
Author: Henri Debrat (henri /dot/ debrat /at/ loria /dot/ fr) and Stephan Merz
Submission date: 2012-07-27
Abstract: Distributed computing is inherently based on replication, promising increased tolerance to failures of individual computing nodes or communication channels. Realizing this promise, however, involves quite subtle algorithmic mechanisms, and requires precise statements about the kinds and numbers of faults that an algorithm tolerates (such as process crashes, communication faults or corrupted values). The landmark theorem due to Fischer, Lynch, and Paterson shows that it is impossible to achieve Consensus among N asynchronously communicating nodes in the presence of even a single permanent failure. Existing solutions must rely on assumptions of "partial synchrony".

Indeed, there have been numerous misunderstandings on what exactly a given algorithm is supposed to realize in what kinds of environments. Moreover, the abundance of subtly different computational models complicates comparisons between different algorithms. Charron-Bost and Schiper introduced the Heard-Of model for representing algorithms and failure assumptions in a uniform framework, simplifying comparisons between algorithms.

In this contribution, we represent the Heard-Of model in Isabelle/HOL. We define two semantics of runs of algorithms with different unit of atomicity and relate these through a reduction theorem that allows us to verify algorithms in the coarse-grained semantics (where proofs are easier) and infer their correctness for the fine-grained one (which corresponds to actual executions). We instantiate the framework by verifying six Consensus algorithms that differ in the underlying algorithmic mechanisms and the kinds of faults they tolerate.

BibTeX: 
@article{Heard_Of-AFP,
   author  = {Henri Debrat and Stephan Merz},
   title   = {Verifying Fault-Tolerant Distributed Algorithms in the Heard-Of Model},
   journal = {Archive of Formal Proofs},
   month   = jul,
   year    = 2012,
   note    = {\url{http://afp.sf.net/entries/Heard_Of.shtml},
             Formal proof development},
   ISSN    = {2150-914x},
 }
License: BSD License
Depends on:Stuttering_Equivalence

">Proof outline
">Proof document
">Browse theories
">Download this entry
Older releases:
diff --git a/web/entries/Hermite.shtml b/web/entries/Hermite.shtml --- a/web/entries/Hermite.shtml +++ b/web/entries/Hermite.shtml @@ -1,115 +1,119 @@ Archive of Formal Proofs

 

Hermite Normal Form

+ + + +
Title: Hermite Normal Form
Author: Jose Divasón and Jesús Aransay
Submission date: 2015-07-07
Abstract: Hermite Normal Form is a canonical matrix analogue of Reduced Echelon Form, but involving matrices over more general rings. In this work we formalise an algorithm to compute the Hermite Normal Form of a matrix by means of elementary row operations, taking advantage of the Echelon Form AFP entry. We have proven the correctness of such an algorithm and refined it to immutable arrays. Furthermore, we have also formalised the uniqueness of the Hermite Normal Form of a matrix. Code can be exported and some examples of execution involving integer matrices and polynomial matrices are presented as well.
BibTeX: 
@article{Hermite-AFP,
   author  = {Jose Divasón and Jesús Aransay},
   title   = {Hermite Normal Form},
   journal = {Archive of Formal Proofs},
   month   = jul,
   year    = 2015,
   note    = {\url{http://afp.sf.net/entries/Hermite.shtml},
             Formal proof development},
   ISSN    = {2150-914x},
 }
License: BSD License
Depends on:Echelon_Form

">Proof outline
">Proof document
">Browse theories
">Download this entry
Older releases:
diff --git a/web/entries/Jinja.shtml b/web/entries/Jinja.shtml --- a/web/entries/Jinja.shtml +++ b/web/entries/Jinja.shtml @@ -1,130 +1,134 @@ Archive of Formal Proofs

 

Jinja is not Java

+ + + +
Title: Jinja is not Java
Author: Gerwin Klein and Tobias Nipkow
Submission date: 2005-06-01
Abstract: We introduce Jinja, a Java-like programming language with a formal semantics designed to exhibit core features of the Java language architecture. Jinja is a compromise between realism of the language and tractability and clarity of the formal semantics. The following aspects are formalised: a big and a small step operational semantics for Jinja and a proof of their equivalence; a type system and a definite initialisation analysis; a type safety proof of the small step semantics; a virtual machine (JVM), its operational semantics and its type system; a type safety proof for the JVM; a bytecode verifier, i.e. data flow analyser for the JVM; a correctness proof of the bytecode verifier w.r.t. the type system; a compiler and a proof that it preserves semantics and well-typedness. The emphasis of this work is not on particular language features but on providing a unified model of the source language, the virtual machine and the compiler. The whole development has been carried out in the theorem prover Isabelle/HOL.
BibTeX: 
@article{Jinja-AFP,
   author  = {Gerwin Klein and Tobias Nipkow},
   title   = {Jinja is not Java},
   journal = {Archive of Formal Proofs},
   month   = jun,
   year    = 2005,
   note    = {\url{http://afp.sf.net/entries/Jinja.shtml},
             Formal proof development},
   ISSN    = {2150-914x},
 }
License: BSD License
Depends on:List-Index

">Proof outline
">Proof document
">Browse theories
">Download this entry
Older releases:
diff --git a/web/entries/JinjaThreads.shtml b/web/entries/JinjaThreads.shtml --- a/web/entries/JinjaThreads.shtml +++ b/web/entries/JinjaThreads.shtml @@ -1,183 +1,183 @@ Archive of Formal Proofs

 

Jinja with Threads

- +
Title: Jinja with Threads
Author: Andreas Lochbihler
Submission date: 2007-12-03
Abstract: We extend the Jinja source code semantics by Klein and Nipkow with Java-style arrays and threads. Concurrency is captured in a generic framework semantics for adding concurrency through interleaving to a sequential semantics, which features dynamic thread creation, inter-thread communication via shared memory, lock synchronisation and joins. Also, threads can suspend themselves and be notified by others. We instantiate the framework with the adapted versions of both Jinja source and byte code and show type safety for the multithreaded case. Equally, the compiler from source to byte code is extended, for which we prove weak bisimilarity between the source code small step semantics and the defensive Jinja virtual machine. On top of this, we formalise the JMM and show the DRF guarantee and consistency. For description of the different parts, see Lochbihler's papers at FOOL 2008, ESOP 2010, ITP 2011, and ESOP 2012.
Change history: [2008-04-23]: added bytecode formalisation with arrays and threads, added thread joins (revision f74a8be156a7)
[2009-04-27]: added verified compiler from source code to bytecode; encapsulate native methods in separate semantics (revision e4f26541e58a)
[2009-11-30]: extended compiler correctness proof to infinite and deadlocking computations (revision e50282397435)
[2010-06-08]: added thread interruption; new abstract memory model with sequential consistency as implementation (revision 0cb9e8dbd78d)
[2010-06-28]: new thread interruption model (revision c0440d0a1177)
[2010-10-15]: preliminary version of the Java memory model for source code (revision 02fee0ef3ca2)
[2010-12-16]: improved version of the Java memory model, also for bytecode executable scheduler for source code semantics (revision 1f41c1842f5a)
[2011-02-02]: simplified code generator setup new random scheduler (revision 3059dafd013f)
[2011-07-21]: new interruption model, generalized JMM proof of DRF guarantee, allow class Object to declare methods and fields, simplified subtyping relation, corrected division and modulo implementation (revision 46e4181ed142)
[2012-02-16]: added example programs (revision bf0b06c8913d)
[2012-11-21]: type safety proof for the Java memory model, allow spurious wake-ups (revision 76063d860ae0)
[2013-05-16]: support for non-deterministic memory allocators (revision cc3344a49ced)
BibTeX: 
@article{JinjaThreads-AFP,
   author  = {Andreas Lochbihler},
   title   = {Jinja with Threads},
   journal = {Archive of Formal Proofs},
   month   = dec,
   year    = 2007,
   note    = {\url{http://afp.sf.net/entries/JinjaThreads.shtml},
             Formal proof development},
   ISSN    = {2150-914x},
 }
License: BSD License
Depends on:Collections, Coinductive
Coinductive, Collections

">Proof outline
">Proof document
">Browse theories
">Download this entry
Older releases:
diff --git a/web/entries/Jordan_Normal_Form.shtml b/web/entries/Jordan_Normal_Form.shtml --- a/web/entries/Jordan_Normal_Form.shtml +++ b/web/entries/Jordan_Normal_Form.shtml @@ -1,139 +1,139 @@ Archive of Formal Proofs

 

Matrices, Jordan Normal Forms, and Spectral Radius Theory

- +
Title: Matrices, Jordan Normal Forms, and Spectral Radius Theory
Author: René Thiemann (rene /dot/ thiemann /at/ uibk /dot/ ac /dot/ at) and Akihisa Yamada (akihisa /dot/ yamada /at/ uibk /dot/ ac /dot/ at)
Submission date: 2015-08-21
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 partially prove the result that every complex matrix has a Jordan normal form: we are restricted to upper-triangular matrices since we did not yet formalize the 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.

Change history: [2016-01-07]: Added Schur-decomposition, Gram-Schmidt orthogonalization, uniqueness of Jordan normal forms
BibTeX: 
@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   = aug,
   year    = 2015,
   note    = {\url{http://afp.sf.net/entries/Jordan_Normal_Form.shtml},
             Formal proof development},
   ISSN    = {2150-914x},
 }
License: BSD License
Depends on:Containers, Gauss_Jordan, Matrix, Abstract-Rewriting, Show, Polynomial_Interpolation, VectorSpace
Matrix, Show, Gauss_Jordan, Polynomial_Interpolation, VectorSpace, Containers, Abstract-Rewriting

">Proof outline
">Proof document
">Browse theories
">Download this entry
Older releases:
diff --git a/web/entries/KBPs.shtml b/web/entries/KBPs.shtml --- a/web/entries/KBPs.shtml +++ b/web/entries/KBPs.shtml @@ -1,128 +1,132 @@ Archive of Formal Proofs

 

Knowledge-based programs

+ + + +
Title: Knowledge-based programs
Author: Peter Gammie
Submission date: 2011-05-17
Abstract: Knowledge-based programs (KBPs) are a formalism for directly relating agents' knowledge and behaviour. Here we present a general scheme for compiling KBPs to executable automata with a proof of correctness in Isabelle/HOL. We develop the algorithm top-down, using Isabelle's locale mechanism to structure these proofs, and show that two classic examples can be synthesised using Isabelle's code generator.
Change history: [2012-03-06]: Add some more views and revive the code generation.
BibTeX: 
@article{KBPs-AFP,
   author  = {Peter Gammie},
   title   = {Knowledge-based programs},
   journal = {Archive of Formal Proofs},
   month   = may,
   year    = 2011,
   note    = {\url{http://afp.sf.net/entries/KBPs.shtml},
             Formal proof development},
   ISSN    = {2150-914x},
 }
License: BSD License
Depends on:Trie, Transitive-Closure

">Proof outline
">Proof document
">Browse theories
">Download this entry
Older releases:
diff --git a/web/entries/LTL_to_DRA.shtml b/web/entries/LTL_to_DRA.shtml --- a/web/entries/LTL_to_DRA.shtml +++ b/web/entries/LTL_to_DRA.shtml @@ -1,131 +1,131 @@ Archive of Formal Proofs

 

Converting Linear Temporal Logic to Deterministic (Generalized) Rabin Automata

- +
Title: Converting Linear Temporal Logic to Deterministic (Generalized) Rabin Automata
Author: Salomon Sickert (sickert /at/ in /dot/ tum /dot/ de)
Submission date: 2015-09-04
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.
Change 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.
BibTeX: 
@article{LTL_to_DRA-AFP,
   author  = {Salomon Sickert},
   title   = {Converting Linear Temporal Logic to Deterministic (Generalized) Rabin Automata},
   journal = {Archive of Formal Proofs},
   month   = sep,
   year    = 2015,
   note    = {\url{http://afp.sf.net/entries/LTL_to_DRA.shtml},
             Formal proof development},
   ISSN    = {2150-914x},
 }
License: BSD License
Depends on:Boolean_Expression_Checkers, List-Index, KBPs
KBPs, List-Index, Boolean_Expression_Checkers

">Proof outline
">Proof document
">Browse theories
">Download this entry
Older releases:
diff --git a/web/entries/LTL_to_GBA.shtml b/web/entries/LTL_to_GBA.shtml --- a/web/entries/LTL_to_GBA.shtml +++ b/web/entries/LTL_to_GBA.shtml @@ -1,137 +1,137 @@ Archive of Formal Proofs

 

Converting Linear-Time Temporal Logic to Generalized Büchi Automata

- +
Title: Converting Linear-Time Temporal Logic to Generalized Büchi Automata
Author: Alexander Schimpf (schimpfa /at/ informatik /dot/ uni-freiburg /dot/ de) and Peter Lammich
Submission date: 2014-05-28
Abstract: We formalize linear-time temporal logic (LTL) and the algorithm by Gerth et al. to convert LTL formulas to generalized Büchi automata. We also formalize some syntactic rewrite rules that can be applied to optimize the LTL formula before conversion. Moreover, we integrate the Stuttering Equivalence AFP-Entry by Stefan Merz, adapting the lemma that next-free LTL formula cannot distinguish between stuttering equivalent runs to our setting.

We use the Isabelle Refinement and Collection framework, as well as the Autoref tool, to obtain a refined version of our algorithm, from which efficiently executable code can be extracted.

BibTeX: 
@article{LTL_to_GBA-AFP,
   author  = {Alexander Schimpf and Peter Lammich},
   title   = {Converting Linear-Time Temporal Logic to Generalized Büchi Automata},
   journal = {Archive of Formal Proofs},
   month   = may,
   year    = 2014,
   note    = {\url{http://afp.sf.net/entries/LTL_to_GBA.shtml},
             Formal proof development},
   ISSN    = {2150-914x},
 }
License: BSD License
Depends on:CAVA_Automata
Deriving, CAVA_Automata, Stuttering_Equivalence

">Proof outline
">Proof document
">Browse theories
">Download this entry
Older releases:
diff --git a/web/entries/Liouville_Numbers.shtml b/web/entries/Liouville_Numbers.shtml --- a/web/entries/Liouville_Numbers.shtml +++ b/web/entries/Liouville_Numbers.shtml @@ -1,128 +1,124 @@ Archive of Formal Proofs

 

Liouville numbers

- - - -
Title: Liouville numbers
Author: Manuel Eberl
Submission date: 2015-12-28
Abstract: Liouville numbers are a class of transcendental numbers that can be approximated particularly well with rational numbers. Historically, they were the first numbers whose transcendence was proven. In this entry, we define the concept of Liouville numbers as well as the standard construction to obtain Liouville numbers (including Liouville's constant) and we prove their most important properties: irrationality and transcendence. The proof is very elementary and requires only standard arithmetic, the Mean Value Theorem for polynomials, and the boundedness of polynomials on compact intervals.
BibTeX: 
@article{Liouville_Numbers-AFP,
   author  = {Manuel Eberl},
   title   = {Liouville numbers},
   journal = {Archive of Formal Proofs},
   month   = dec,
   year    = 2015,
   note    = {\url{http://afp.sf.net/entries/Liouville_Numbers.shtml},
             Formal proof development},
   ISSN    = {2150-914x},
 }
License: BSD License
Depends on:Algebraic_Numbers

">Proof outline
">Proof document
">Browse theories
">Download this entry
Older releases:
diff --git a/web/entries/MSO_Regex_Equivalence.shtml b/web/entries/MSO_Regex_Equivalence.shtml --- a/web/entries/MSO_Regex_Equivalence.shtml +++ b/web/entries/MSO_Regex_Equivalence.shtml @@ -1,143 +1,147 @@ Archive of Formal Proofs

 

Decision Procedures for MSO on Words Based on Derivatives of Regular Expressions

+ + + +
Title: Decision Procedures for MSO on Words Based on Derivatives of Regular Expressions
Author: Dmitriy Traytel (traytel /at/ in /dot/ tum /dot/ de) and Tobias Nipkow
Submission date: 2014-06-12
Abstract: Monadic second-order logic on finite words (MSO) is a decidable yet expressive logic into which many decision problems can be encoded. Since MSO formulas correspond to regular languages, equivalence of MSO formulas can be reduced to the equivalence of some regular structures (e.g. automata). We verify an executable decision procedure for MSO formulas that is not based on automata but on regular expressions.

Decision procedures for regular expression equivalence have been formalized before, usually based on Brzozowski derivatives. Yet, for a straightforward embedding of MSO formulas into regular expressions an extension of regular expressions with a projection operation is required. We prove total correctness and completeness of an equivalence checker for regular expressions extended in that way. We also define a language-preserving translation of formulas into regular expressions with respect to two different semantics of MSO.

The formalization is described in this ICFP 2013 functional pearl.

BibTeX: 
@article{MSO_Regex_Equivalence-AFP,
   author  = {Dmitriy Traytel and Tobias Nipkow},
   title   = {Decision Procedures for MSO on Words Based on Derivatives of Regular Expressions},
   journal = {Archive of Formal Proofs},
   month   = jun,
   year    = 2014,
   note    = {\url{http://afp.sf.net/entries/MSO_Regex_Equivalence.shtml},
             Formal proof development},
   ISSN    = {2150-914x},
 }
License: BSD License
Depends on:Deriving, List-Index

">Proof outline
">Proof document
">Browse theories
">Download this entry
Older releases:
diff --git a/web/entries/Markov_Models.shtml b/web/entries/Markov_Models.shtml --- a/web/entries/Markov_Models.shtml +++ b/web/entries/Markov_Models.shtml @@ -1,129 +1,133 @@ Archive of Formal Proofs

 

Markov Models

+ + + +
Title: Markov Models
Author: Johannes Hölzl and Tobias Nipkow
Submission date: 2012-01-03
Abstract: This is a formalization of Markov models in Isabelle/HOL. It builds on Isabelle's probability theory. The available models are currently Discrete-Time Markov Chains and a extensions of them with rewards.

As application of these models we formalize probabilistic model checking of pCTL formulas, analysis of IPv4 address allocation in ZeroConf and an analysis of the anonymity of the Crowds protocol. See here for the corresponding paper.

BibTeX: 
@article{Markov_Models-AFP,
   author  = {Johannes Hölzl and Tobias Nipkow},
   title   = {Markov Models},
   journal = {Archive of Formal Proofs},
   month   = jan,
   year    = 2012,
   note    = {\url{http://afp.sf.net/entries/Markov_Models.shtml},
             Formal proof development},
   ISSN    = {2150-914x},
 }
License: BSD License
Depends on:Coinductive, Gauss-Jordan-Elim-Fun

">Proof outline
">Proof document
">Browse theories
">Download this entry
Older releases:
diff --git a/web/entries/MonoBoolTranAlgebra.shtml b/web/entries/MonoBoolTranAlgebra.shtml --- a/web/entries/MonoBoolTranAlgebra.shtml +++ b/web/entries/MonoBoolTranAlgebra.shtml @@ -1,124 +1,128 @@ Archive of Formal Proofs

 

Algebra of Monotonic Boolean Transformers

+ + + +
Title: Algebra of Monotonic Boolean Transformers
Author: Viorel Preoteasa
Submission date: 2011-09-22
Abstract: Algebras of imperative programming languages have been successful in reasoning about programs. In general an algebra of programs is an algebraic structure with programs as elements and with program compositions (sequential composition, choice, skip) as algebra operations. Various versions of these algebras were introduced to model partial correctness, total correctness, refinement, demonic choice, and other aspects. We formalize here an algebra which can be used to model total correctness, refinement, demonic and angelic choice. The basic model of this algebra are monotonic Boolean transformers (monotonic functions from a Boolean algebra to itself).
BibTeX: 
@article{MonoBoolTranAlgebra-AFP,
   author  = {Viorel Preoteasa},
   title   = {Algebra of Monotonic Boolean Transformers},
   journal = {Archive of Formal Proofs},
   month   = sep,
   year    = 2011,
   note    = {\url{http://afp.sf.net/entries/MonoBoolTranAlgebra.shtml},
             Formal proof development},
   ISSN    = {2150-914x},
 }
License: BSD License
Depends on:LatticeProperties

">Proof outline
">Proof document
">Browse theories
">Download this entry
Older releases:
diff --git a/web/entries/Myhill-Nerode.shtml b/web/entries/Myhill-Nerode.shtml --- a/web/entries/Myhill-Nerode.shtml +++ b/web/entries/Myhill-Nerode.shtml @@ -1,126 +1,130 @@ Archive of Formal Proofs

 

The Myhill-Nerode Theorem Based on Regular Expressions

+ + + +
Title: The Myhill-Nerode Theorem Based on Regular Expressions
Author: Chunhan Wu, Xingyuan Zhang and Christian Urban
Submission date: 2011-08-26
Abstract: There are many proofs of the Myhill-Nerode theorem using automata. In this library we give a proof entirely based on regular expressions, since regularity of languages can be conveniently defined using regular expressions (it is more painful in HOL to define regularity in terms of automata). We prove the first direction of the Myhill-Nerode theorem by solving equational systems that involve regular expressions. For the second direction we give two proofs: one using tagging-functions and another using partial derivatives. We also establish various closure properties of regular languages. Most details of the theories are described in our ITP 2011 paper.
BibTeX: 
@article{Myhill-Nerode-AFP,
   author  = {Chunhan Wu and Xingyuan Zhang and Christian Urban},
   title   = {The Myhill-Nerode Theorem Based on Regular Expressions},
   journal = {Archive of Formal Proofs},
   month   = aug,
   year    = 2011,
   note    = {\url{http://afp.sf.net/entries/Myhill-Nerode.shtml},
             Formal proof development},
   ISSN    = {2150-914x},
 }
License: BSD License
Depends on:Well_Quasi_Orders, Regular-Sets

">Proof outline
">Proof document
">Browse theories
">Download this entry
Older releases:
diff --git a/web/entries/Network_Security_Policy_Verification.shtml b/web/entries/Network_Security_Policy_Verification.shtml --- a/web/entries/Network_Security_Policy_Verification.shtml +++ b/web/entries/Network_Security_Policy_Verification.shtml @@ -1,160 +1,164 @@ Archive of Formal Proofs

 

Network Security Policy Verification

+ + + +
Title: Network Security Policy Verification
Author: Cornelius Diekmann
Submission date: 2014-07-04
Abstract: We present a unified theory for verifying network security policies. A security policy is represented as directed graph. To check high-level security goals, security invariants over the policy are expressed. We cover monotonic security invariants, i.e. prohibiting more does not harm security. We provide the following contributions for the security invariant theory.
  • Secure auto-completion of scenario-specific knowledge, which eases usability.
  • Security violations can be repaired by tightening the policy iff the security invariants hold for the deny-all policy.
  • An algorithm to compute a security policy.
  • A formalization of stateful connection semantics in network security mechanisms.
  • An algorithm to compute a secure stateful implementation of a policy.
  • An executable implementation of all the theory.
  • Examples, ranging from an aircraft cabin data network to the analysis of a large real-world firewall.
  • More examples: A fully automated translation of high-level security goals to both firewall and SDN configurations (see Examples/Distributed_WebApp.thy).
For a detailed description, see
Change history: [2015-04-14]: Added Distributed WebApp example and improved graphviz visualization (revision 4dde08ca2ab8)
BibTeX: 
@article{Network_Security_Policy_Verification-AFP,
   author  = {Cornelius Diekmann},
   title   = {Network Security Policy Verification},
   journal = {Archive of Formal Proofs},
   month   = jul,
   year    = 2014,
   note    = {\url{http://afp.sf.net/entries/Network_Security_Policy_Verification.shtml},
             Formal proof development},
   ISSN    = {2150-914x},
 }
License: BSD License
Depends on:Transitive-Closure, Collections, Automatic_Refinement

">Proof outline
">Proof document
">Browse theories
">Download this entry
Older releases:
diff --git a/web/entries/Open_Induction.shtml b/web/entries/Open_Induction.shtml --- a/web/entries/Open_Induction.shtml +++ b/web/entries/Open_Induction.shtml @@ -1,121 +1,125 @@ Archive of Formal Proofs

 

Open Induction

+ + + +
Title: Open Induction
Author: Mizuhito Ogawa and Christian Sternagel
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://afp.sf.net/entries/Open_Induction.shtml},
             Formal proof development},
   ISSN    = {2150-914x},
 }
License: BSD License
Depends on:Well_Quasi_Orders

">Proof outline
">Proof document
">Browse theories
">Download this entry
Older releases:
diff --git a/web/entries/Ordinary_Differential_Equations.shtml b/web/entries/Ordinary_Differential_Equations.shtml --- a/web/entries/Ordinary_Differential_Equations.shtml +++ b/web/entries/Ordinary_Differential_Equations.shtml @@ -1,126 +1,130 @@ Archive of Formal Proofs

 

Ordinary Differential Equations

+ + + +
Title: Ordinary Differential Equations
Author: Fabian Immler and Johannes Hölzl
Submission date: 2012-04-26
Abstract: We formalize initial value problems (IVPs) of ODEs and prove the existence of a unique solution, i.e. the Picard-Lindelöf theorem. We introduce general one-step methods for numerical approximation of the solution and provide an analysis regarding the local and global error of one-step methods. We give an executable specification of the Euler method to approximate the solution of IVPs and prove an explicit bound for the global error. We use arbitrary-precision floating-point numbers and also handle rounding errors when we truncate the numbers for efficiency reasons.
Change history: [2014-02-13]: added an implementation of the Euler method based on affine arithmetic
BibTeX: 
@article{Ordinary_Differential_Equations-AFP,
   author  = {Fabian Immler and Johannes Hölzl},
   title   = {Ordinary Differential Equations},
   journal = {Archive of Formal Proofs},
   month   = apr,
   year    = 2012,
   note    = {\url{http://afp.sf.net/entries/Ordinary_Differential_Equations.shtml},
             Formal proof development},
   ISSN    = {2150-914x},
 }
License: BSD License
Depends on:Affine_Arithmetic

">Proof outline
">Proof document
">Browse theories
">Download this entry
Older releases:
diff --git a/web/entries/Planarity_Certificates.shtml b/web/entries/Planarity_Certificates.shtml --- a/web/entries/Planarity_Certificates.shtml +++ b/web/entries/Planarity_Certificates.shtml @@ -1,121 +1,121 @@ Archive of Formal Proofs

 

Planarity Certificates

- +
Title: Planarity Certificates
Author: Lars Noschinski
Submission date: 2015-11-11
Abstract: This development provides a formalization of planarity based on combinatorial maps and proves that Kuratowski's theorem implies combinatorial planarity. Moreover, it contains verified implementations of programs checking certificates for planarity (i.e., a combinatorial map) or non-planarity (i.e., a Kuratowski subgraph).
BibTeX: 
@article{Planarity_Certificates-AFP,
   author  = {Lars Noschinski},
   title   = {Planarity Certificates},
   journal = {Archive of Formal Proofs},
   month   = nov,
   year    = 2015,
   note    = {\url{http://afp.sf.net/entries/Planarity_Certificates.shtml},
             Formal proof development},
   ISSN    = {2150-914x},
 }
License: BSD License
Depends on:Simpl, Case_Labeling, Graph_Theory, List-Index, Transitive-Closure
Case_Labeling, Transitive-Closure, Graph_Theory, Simpl, List-Index

">Proof outline
">Proof document
">Browse theories
">Download this entry
Older releases: None
diff --git a/web/entries/Polynomial_Factorization.shtml b/web/entries/Polynomial_Factorization.shtml --- a/web/entries/Polynomial_Factorization.shtml +++ b/web/entries/Polynomial_Factorization.shtml @@ -1,129 +1,129 @@ Archive of Formal Proofs

 

Polynomial Factorization

- +
Title: Polynomial Factorization
Author: René Thiemann (rene /dot/ thiemann /at/ uibk /dot/ ac /dot/ at) and Akihisa Yamada (akihisa /dot/ yamada /at/ uibk /dot/ ac /dot/ at)
Submission date: 2016-01-29
Abstract: Based on existing libraries for polynomial interpolation and matrices, we formalized several factorization algorithms for polynomials, including Kronecker's algorithm for integer polynomials, Yun's square-free factorization algorithm for field polynomials, and Berlekamp's algorithm for polynomials over finite fields. By combining the last one with Hensel's lifting, we derive an efficient factorization algorithm for the integer polynomials, which is then lifted for rational polynomials by mechanizing Gauss' lemma. Finally, we assembled a combined factorization algorithm for rational polynomials, which combines all the mentioned algorithms and additionally uses the explicit formula for roots of quadratic polynomials and a rational root test.

As side products, we developed division algorithms for polynomials over integral domains, as well as primality-testing and prime-factorization algorithms for integers.

BibTeX: 
@article{Polynomial_Factorization-AFP,
   author  = {René Thiemann and Akihisa Yamada},
   title   = {Polynomial Factorization},
   journal = {Archive of Formal Proofs},
   month   = jan,
   year    = 2016,
   note    = {\url{http://afp.sf.net/entries/Polynomial_Factorization.shtml},
             Formal proof development},
   ISSN    = {2150-914x},
 }
License: BSD License
Depends on:Polynomial_Interpolation, Partial_Function_MR, Sqrt_Babylonian, Show, Jordan_Normal_Form
Matrix, Show, Sqrt_Babylonian, Polynomial_Interpolation, Partial_Function_MR, Jordan_Normal_Form, Containers

">Proof outline
">Proof document
">Browse theories
">Download this entry
Older releases: None
diff --git a/web/entries/Polynomials.shtml b/web/entries/Polynomials.shtml --- a/web/entries/Polynomials.shtml +++ b/web/entries/Polynomials.shtml @@ -1,144 +1,144 @@ Archive of Formal Proofs

 

Executable Multivariate Polynomials

- +
Title: Executable Multivariate Polynomials
Author: Christian Sternagel and René Thiemann
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.
Change history: [2010-09-17]: Moved theories on arbitrary (ordered) semirings to Abstract Rewriting.
BibTeX: 
@article{Polynomials-AFP,
   author  = {Christian Sternagel and René Thiemann},
   title   = {Executable Multivariate Polynomials},
   journal = {Archive of Formal Proofs},
   month   = aug,
   year    = 2010,
   note    = {\url{http://afp.sf.net/entries/Polynomials.shtml},
             Formal proof development},
   ISSN    = {2150-914x},
 }
License: GNU Lesser General Public License (LGPL)
Depends on:Abstract-Rewriting
Abstract-Rewriting, Matrix

">Proof outline
">Proof document
">Browse theories
">Download this entry
Older releases:
diff --git a/web/entries/Probabilistic_Noninterference.shtml b/web/entries/Probabilistic_Noninterference.shtml --- a/web/entries/Probabilistic_Noninterference.shtml +++ b/web/entries/Probabilistic_Noninterference.shtml @@ -1,116 +1,120 @@ Archive of Formal Proofs

 

Probabilistic Noninterference

+ + + +
Title: Probabilistic Noninterference
Author: Andrei Popescu and Johannes Hölzl
Submission date: 2014-03-11
Abstract: We formalize a probabilistic noninterference for a multi-threaded language with uniform scheduling, where probabilistic behaviour comes from both the scheduler and the individual threads. We define notions probabilistic noninterference in two variants: resumption-based and trace-based. For the resumption-based notions, we prove compositionality w.r.t. the language constructs and establish sound type-system-like syntactic criteria. This is a formalization of the mathematical development presented at CPP 2013 and CALCO 2013. It is the probabilistic variant of the Possibilistic Noninterference AFP entry.
BibTeX: 
@article{Probabilistic_Noninterference-AFP,
   author  = {Andrei Popescu and Johannes Hölzl},
   title   = {Probabilistic Noninterference},
   journal = {Archive of Formal Proofs},
   month   = mar,
   year    = 2014,
   note    = {\url{http://afp.sf.net/entries/Probabilistic_Noninterference.shtml},
             Formal proof development},
   ISSN    = {2150-914x},
 }
License: BSD License
Depends on:Markov_Models

">Proof outline
">Proof document
">Browse theories
">Download this entry
Older releases:
diff --git a/web/entries/Promela.shtml b/web/entries/Promela.shtml --- a/web/entries/Promela.shtml +++ b/web/entries/Promela.shtml @@ -1,130 +1,130 @@ Archive of Formal Proofs

 

Promela Formalization

- +
Title: Promela Formalization
Author: René Neumann (rene /dot/ neumann /at/ in /dot/ tum /dot/ de)
Submission date: 2014-05-28
Abstract: We present an executable formalization of the language Promela, the description lasebastien.gouezel@univ-rennes1.frnguage for models of the model checker SPIN. This formalization is part of the work for a completely verified model checker (CAVA), but also serves as a useful (and executable!) description of the semantics of the language itself, something that is currently missing. The formalization uses three steps: It takes an abstract syntax tree generated from an SML parser, removes syntactic sugar and enriches it with type information. This further gets translated into a transition system, on which the semantic engine (read: successor function) operates.
BibTeX: 
@article{Promela-AFP,
   author  = {René Neumann},
   title   = {Promela Formalization},
   journal = {Archive of Formal Proofs},
   month   = may,
   year    = 2014,
   note    = {\url{http://afp.sf.net/entries/Promela.shtml},
             Formal proof development},
   ISSN    = {2150-914x},
 }
License: BSD License
Depends on:CAVA_Automata
Deriving, CAVA_Automata, LTL_to_GBA

">Proof outline
">Proof document
">Browse theories
">Download this entry
Older releases:
diff --git a/web/entries/PseudoHoops.shtml b/web/entries/PseudoHoops.shtml --- a/web/entries/PseudoHoops.shtml +++ b/web/entries/PseudoHoops.shtml @@ -1,121 +1,125 @@ Archive of Formal Proofs

 

Pseudo Hoops

+ + + +
Title: Pseudo Hoops
Author: George Georgescu, Laurentiu Leustean and Viorel Preoteasa
Submission date: 2011-09-22
Abstract: Pseudo-hoops are algebraic structures introduced by B. Bosbach under the name of complementary semigroups. In this formalization we prove some properties of pseudo-hoops and we define the basic concepts of filter and normal filter. The lattice of normal filters is isomorphic with the lattice of congruences of a pseudo-hoop. We also study some important classes of pseudo-hoops. Bounded Wajsberg pseudo-hoops are equivalent to pseudo-Wajsberg algebras and bounded basic pseudo-hoops are equivalent to pseudo-BL algebras. Some examples of pseudo-hoops are given in the last section of the formalization.
BibTeX: 
@article{PseudoHoops-AFP,
   author  = {George Georgescu and Laurentiu Leustean and Viorel Preoteasa},
   title   = {Pseudo Hoops},
   journal = {Archive of Formal Proofs},
   month   = sep,
   year    = 2011,
   note    = {\url{http://afp.sf.net/entries/PseudoHoops.shtml},
             Formal proof development},
   ISSN    = {2150-914x},
 }
License: BSD License
Depends on:LatticeProperties

">Proof outline
">Proof document
">Browse theories
">Download this entry
Older releases:
diff --git a/web/entries/QR_Decomposition.shtml b/web/entries/QR_Decomposition.shtml --- a/web/entries/QR_Decomposition.shtml +++ b/web/entries/QR_Decomposition.shtml @@ -1,121 +1,125 @@ Archive of Formal Proofs

 

QR Decomposition

+ + + +
Title: QR Decomposition
Author: Jose Divasón and Jesús Aransay
Submission date: 2015-02-12
Abstract: QR decomposition is an algorithm to decompose a real matrix A into the product of two other matrices Q and R, where Q is orthogonal and R is invertible and upper triangular. The algorithm is useful for the least squares problem; i.e., the computation of the best approximation of an unsolvable system of linear equations. As a side-product, the Gram-Schmidt process has also been formalized. A refinement using immutable arrays is presented as well. The development relies, among others, on the AFP entry "Implementing field extensions of the form Q[sqrt(b)]" by René Thiemann, which allows execution of the algorithm using symbolic computations. Verified code can be generated and executed using floats as well.
Change history: [2015-06-18]: The second part of the Fundamental Theorem of Linear Algebra has been generalized to more general inner product spaces.
BibTeX: 
@article{QR_Decomposition-AFP,
   author  = {Jose Divasón and Jesús Aransay},
   title   = {QR Decomposition},
   journal = {Archive of Formal Proofs},
   month   = feb,
   year    = 2015,
   note    = {\url{http://afp.sf.net/entries/QR_Decomposition.shtml},
             Formal proof development},
   ISSN    = {2150-914x},
 }
License: BSD License
Depends on:Real_Impl, Rank_Nullity_Theorem, Gauss_Jordan

">Proof outline
">Proof document
">Browse theories
">Download this entry
Older releases:
diff --git a/web/entries/Random_Graph_Subgraph_Threshold.shtml b/web/entries/Random_Graph_Subgraph_Threshold.shtml --- a/web/entries/Random_Graph_Subgraph_Threshold.shtml +++ b/web/entries/Random_Graph_Subgraph_Threshold.shtml @@ -1,121 +1,125 @@ Archive of Formal Proofs

 

Properties of Random Graphs -- Subgraph Containment

+ + + +
Title: Properties of Random Graphs -- Subgraph Containment
Author: Lars Hupel (hupel /at/ in /dot/ tum /dot/ de)
Submission date: 2014-02-13
Abstract: Random graphs are graphs with a fixed number of vertices, where each edge is present with a fixed probability. We are interested in the probability that a random graph contains a certain pattern, for example a cycle or a clique. A very high edge probability gives rise to perhaps too many edges (which degrades performance for many algorithms), whereas a low edge probability might result in a disconnected graph. We prove a theorem about a threshold probability such that a higher edge probability will asymptotically almost surely produce a random graph with the desired subgraph.
BibTeX: 
@article{Random_Graph_Subgraph_Threshold-AFP,
   author  = {Lars Hupel},
   title   = {Properties of Random Graphs -- Subgraph Containment},
   journal = {Archive of Formal Proofs},
   month   = feb,
   year    = 2014,
   note    = {\url{http://afp.sf.net/entries/Random_Graph_Subgraph_Threshold.shtml},
             Formal proof development},
   ISSN    = {2150-914x},
 }
License: BSD License
Depends on:Girth_Chromatic

">Proof outline
">Proof document
">Browse theories
">Download this entry
Older releases:
diff --git a/web/entries/Real_Impl.shtml b/web/entries/Real_Impl.shtml --- a/web/entries/Real_Impl.shtml +++ b/web/entries/Real_Impl.shtml @@ -1,136 +1,140 @@ Archive of Formal Proofs

 

Implementing field extensions of the form Q[sqrt(b)]

+ + + +
Title: Implementing field extensions of the form Q[sqrt(b)]
Author: René Thiemann (rene /dot/ thiemann /at/ uibk /dot/ ac /dot/ at)
Submission date: 2014-02-06
Abstract: We apply data refinement to implement the real numbers, where we support all numbers in the field extension Q[sqrt(b)], i.e., all numbers of the form p + q * sqrt(b) for rational numbers p and q and some fixed natural number b. To this end, we also developed algorithms to precisely compute roots of a rational number, and to perform a factorization of natural numbers which eliminates duplicate prime factors.

Our results have been used to certify termination proofs which involve polynomial interpretations over the reals.

Change history: [2014-07-11]: Moved NthRoot_Impl to Sqrt-Babylonian.
BibTeX: 
@article{Real_Impl-AFP,
   author  = {René Thiemann},
   title   = {Implementing field extensions of the form Q[sqrt(b)]},
   journal = {Archive of Formal Proofs},
   month   = feb,
   year    = 2014,
   note    = {\url{http://afp.sf.net/entries/Real_Impl.shtml},
             Formal proof development},
   ISSN    = {2150-914x},
 }
License: GNU Lesser General Public License (LGPL)
Depends on:Sqrt_Babylonian, Show

">Proof outline
">Proof document
">Browse theories
">Download this entry
Older releases:
diff --git a/web/entries/Regex_Equivalence.shtml b/web/entries/Regex_Equivalence.shtml --- a/web/entries/Regex_Equivalence.shtml +++ b/web/entries/Regex_Equivalence.shtml @@ -1,133 +1,137 @@ Archive of Formal Proofs

 

Unified Decision Procedures for Regular Expression Equivalence

+ + + +
Title: Unified Decision Procedures for Regular Expression Equivalence
Author: Tobias Nipkow and Dmitriy Traytel (traytel /at/ in /dot/ tum /dot/ de)
Submission date: 2014-01-30
Abstract: We formalize a unified framework for verified decision procedures for regular expression equivalence. Five recently published formalizations of such decision procedures (three based on derivatives, two on marked regular expressions) can be obtained as instances of the framework. We discover that the two approaches based on marked regular expressions, which were previously thought to be the same, are different, and one seems to produce uniformly smaller automata. The common framework makes it possible to compare the performance of the different decision procedures in a meaningful way. The formalization is described in a paper of the same name presented at Interactive Theorem Proving 2014.
BibTeX: 
@article{Regex_Equivalence-AFP,
   author  = {Tobias Nipkow and Dmitriy Traytel},
   title   = {Unified Decision Procedures for Regular Expression Equivalence},
   journal = {Archive of Formal Proofs},
   month   = jan,
   year    = 2014,
   note    = {\url{http://afp.sf.net/entries/Regex_Equivalence.shtml},
             Formal proof development},
   ISSN    = {2150-914x},
 }
License: BSD License
Depends on:Efficient-Mergesort, Regular-Sets

">Proof outline
">Proof document
">Browse theories
">Download this entry
Older releases:
diff --git a/web/entries/Residuated_Lattices.shtml b/web/entries/Residuated_Lattices.shtml --- a/web/entries/Residuated_Lattices.shtml +++ b/web/entries/Residuated_Lattices.shtml @@ -1,126 +1,126 @@ Archive of Formal Proofs

 

Residuated Lattices

- +
Title: Residuated Lattices
Author: Victor B. F. Gomes (vborgesferreiragomes1 /at/ sheffield /dot/ ac /dot/ uk) and Georg Struth (g /dot/ struth /at/ sheffield /dot/ ac /dot/ uk)
Submission date: 2015-04-15
Abstract: The theory of residuated lattices, first proposed by Ward and Dilworth, is formalised in Isabelle/HOL. This includes concepts of residuated functions; their adjoints and conjugates. It also contains necessary and sufficient conditions for the existence of these operations in an arbitrary lattice. The mathematical components for residuated lattices are linked to the AFP entry for relation algebra. In particular, we prove Jonsson and Tsinakis conditions for a residuated boolean algebra to form a relation algebra.
BibTeX: 
@article{Residuated_Lattices-AFP,
   author  = {Victor B. F. Gomes and Georg Struth},
   title   = {Residuated Lattices},
   journal = {Archive of Formal Proofs},
   month   = apr,
   year    = 2015,
   note    = {\url{http://afp.sf.net/entries/Residuated_Lattices.shtml},
             Formal proof development},
   ISSN    = {2150-914x},
 }
License: BSD License
Depends on:Relation_Algebra
Relation_Algebra, Kleene_Algebra

">Proof outline
">Proof document
">Browse theories
">Download this entry
Older releases:
diff --git a/web/entries/Separation_Logic_Imperative_HOL.shtml b/web/entries/Separation_Logic_Imperative_HOL.shtml --- a/web/entries/Separation_Logic_Imperative_HOL.shtml +++ b/web/entries/Separation_Logic_Imperative_HOL.shtml @@ -1,137 +1,141 @@ Archive of Formal Proofs

 

A Separation Logic Framework for Imperative HOL

+ + + +
Title: A Separation Logic Framework for Imperative HOL
Author: Peter Lammich and Rene Meis (rene /dot/ meis /at/ uni-due /dot/ de)
Submission date: 2012-11-14
Abstract: We provide a framework for separation-logic based correctness proofs of Imperative HOL programs. Our framework comes with a set of proof methods to automate canonical tasks such as verification condition generation and frame inference. Moreover, we provide a set of examples that show the applicability of our framework. The examples include algorithms on lists, hash-tables, and union-find trees. We also provide abstract interfaces for lists, maps, and sets, that allow to develop generic imperative algorithms and use data-refinement techniques.
As we target Imperative HOL, our programs can be translated to efficiently executable code in various target languages, including ML, OCaml, Haskell, and Scala.
BibTeX: 
@article{Separation_Logic_Imperative_HOL-AFP,
   author  = {Peter Lammich and Rene Meis},
   title   = {A Separation Logic Framework for Imperative HOL},
   journal = {Archive of Formal Proofs},
   month   = nov,
   year    = 2012,
   note    = {\url{http://afp.sf.net/entries/Separation_Logic_Imperative_HOL.shtml},
             Formal proof development},
   ISSN    = {2150-914x},
 }
License: BSD License
Depends on:Collections, Automatic_Refinement

">Proof outline
">Proof document
">Browse theories
">Download this entry
Older releases:
diff --git a/web/entries/ShortestPath.shtml b/web/entries/ShortestPath.shtml --- a/web/entries/ShortestPath.shtml +++ b/web/entries/ShortestPath.shtml @@ -1,125 +1,129 @@ Archive of Formal Proofs

 

An Axiomatic Characterization of the Single-Source Shortest Path Problem

+ + + +
Title: An Axiomatic Characterization of the Single-Source Shortest Path Problem
Author: Christine Rizkallah
Submission date: 2013-05-22
Abstract: This theory is split into two sections. In the first section, we give a formal proof that a well-known axiomatic characterization of the single-source shortest path problem is correct. Namely, we prove that in a directed graph with a non-negative cost function on the edges the single-source shortest path function is the only function that satisfies a set of four axioms. In the second section, we give a formal proof of the correctness of an axiomatic characterization of the single-source shortest path problem for directed graphs with general cost functions. The axioms here are more involved because we have to account for potential negative cycles in the graph. The axioms are summarized in three Isabelle locales.
BibTeX: 
@article{ShortestPath-AFP,
   author  = {Christine Rizkallah},
   title   = {An Axiomatic Characterization of the Single-Source Shortest Path Problem},
   journal = {Archive of Formal Proofs},
   month   = may,
   year    = 2013,
   note    = {\url{http://afp.sf.net/entries/ShortestPath.shtml},
             Formal proof development},
   ISSN    = {2150-914x},
 }
License: BSD License
Depends on:Graph_Theory

">Proof outline
">Proof document
">Browse theories
">Download this entry
Older releases:
diff --git a/web/entries/Show.shtml b/web/entries/Show.shtml --- a/web/entries/Show.shtml +++ b/web/entries/Show.shtml @@ -1,136 +1,136 @@ Archive of Formal Proofs

 

Haskell's Show Class in Isabelle/HOL

- +
Title: Haskell's Show Class in Isabelle/HOL
Author: Christian Sternagel (c /dot/ sternagel /at/ gmail /dot/ com) and René Thiemann (rene /dot/ thiemann /at/ uibk /dot/ ac /dot/ at)
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://afp.sf.net/entries/Show.shtml},
             Formal proof development},
   ISSN    = {2150-914x},
 }
License: GNU Lesser General Public License (LGPL)
Depends on:Datatype_Order_Generator, Deriving
Deriving, Datatype_Order_Generator

">Proof outline
">Proof document
">Browse theories
">Download this entry
Older releases:
diff --git a/web/entries/Special_Function_Bounds.shtml b/web/entries/Special_Function_Bounds.shtml --- a/web/entries/Special_Function_Bounds.shtml +++ b/web/entries/Special_Function_Bounds.shtml @@ -1,121 +1,125 @@ Archive of Formal Proofs

 

Real-Valued Special Functions: Upper and Lower Bounds

+ + + +
Title: Real-Valued Special Functions: Upper and Lower Bounds
Author: Lawrence C. Paulson
Submission date: 2014-08-29
Abstract: This development proves upper and lower bounds for several familiar real-valued functions. For sin, cos, exp and sqrt, it defines and verifies infinite families of upper and lower bounds, mostly based on Taylor series expansions. For arctan, ln and exp, it verifies a finite collection of upper and lower bounds, originally obtained from the functions' continued fraction expansions using the computer algebra system Maple. A common theme in these proofs is to take the difference between a function and its approximation, which should be zero at one point, and then consider the sign of the derivative. The immediate purpose of this development is to verify axioms used by MetiTarski, an automatic theorem prover for real-valued special functions. Crucial to MetiTarski's operation is the provision of upper and lower bounds for each function of interest.
BibTeX: 
@article{Special_Function_Bounds-AFP,
   author  = {Lawrence C. Paulson},
   title   = {Real-Valued Special Functions: Upper and Lower Bounds},
   journal = {Archive of Formal Proofs},
   month   = aug,
   year    = 2014,
   note    = {\url{http://afp.sf.net/entries/Special_Function_Bounds.shtml},
             Formal proof development},
   ISSN    = {2150-914x},
 }
License: BSD License
Depends on:Sturm_Sequences

">Proof outline
">Proof document
">Browse theories
">Download this entry
Older releases:
diff --git a/web/entries/Sqrt_Babylonian.shtml b/web/entries/Sqrt_Babylonian.shtml --- a/web/entries/Sqrt_Babylonian.shtml +++ b/web/entries/Sqrt_Babylonian.shtml @@ -1,135 +1,139 @@ Archive of Formal Proofs

 

Computing N-th Roots using the Babylonian Method

+ + + +
Title: Computing N-th Roots using the Babylonian Method
Author: René Thiemann (rene /dot/ thiemann /at/ uibk /dot/ ac /dot/ at)
Submission date: 2013-01-03
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.
Change history: [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.
BibTeX: 
@article{Sqrt_Babylonian-AFP,
   author  = {René Thiemann},
   title   = {Computing N-th Roots using the Babylonian Method},
   journal = {Archive of Formal Proofs},
   month   = jan,
   year    = 2013,
   note    = {\url{http://afp.sf.net/entries/Sqrt_Babylonian.shtml},
             Formal proof development},
   ISSN    = {2150-914x},
 }
License: GNU Lesser General Public License (LGPL)
Depends on:Cauchy

">Proof outline
">Proof document
">Browse theories
">Download this entry
Older releases:
diff --git a/web/entries/Stream_Fusion_Code.shtml b/web/entries/Stream_Fusion_Code.shtml --- a/web/entries/Stream_Fusion_Code.shtml +++ b/web/entries/Stream_Fusion_Code.shtml @@ -1,121 +1,125 @@ Archive of Formal Proofs

 

Stream Fusion in HOL with Code Generation

+ + + +
Title: Stream Fusion in HOL with Code Generation
Author: Andreas Lochbihler and Alexandra Maximova (amaximov /at/ student /dot/ ethz /dot/ ch)
Submission date: 2014-10-10
Abstract: Stream Fusion is a system for removing intermediate list data structures from functional programs, in particular Haskell. This entry adapts stream fusion to Isabelle/HOL and its code generator. We define stream types for finite and possibly infinite lists and stream versions for most of the fusible list functions in the theories List and Coinductive_List, and prove them correct with respect to the conversion functions between lists and streams. The Stream Fusion transformation itself is implemented as a simproc in the preprocessor of the code generator. [Brian Huffman's AFP entry formalises stream fusion in HOLCF for the domain of lazy lists to prove the GHC compiler rewrite rules correct. In contrast, this work enables Isabelle's code generator to perform stream fusion itself. To that end, it covers both finite and coinductive lists from the HOL library and the Coinductive entry. The fusible list functions require specification and proof principles different from Huffman's.]
BibTeX: 
@article{Stream_Fusion_Code-AFP,
   author  = {Andreas Lochbihler and Alexandra Maximova},
   title   = {Stream Fusion in HOL with Code Generation},
   journal = {Archive of Formal Proofs},
   month   = oct,
   year    = 2014,
   note    = {\url{http://afp.sf.net/entries/Stream_Fusion_Code.shtml},
             Formal proof development},
   ISSN    = {2150-914x},
 }
License: BSD License
Depends on:Coinductive

">Proof outline
">Proof document
">Browse theories
">Download this entry
Older releases:
diff --git a/web/entries/Transitive-Closure.shtml b/web/entries/Transitive-Closure.shtml --- a/web/entries/Transitive-Closure.shtml +++ b/web/entries/Transitive-Closure.shtml @@ -1,136 +1,136 @@ Archive of Formal Proofs

 

Executable Transitive Closures of Finite Relations

- +
Title: Executable Transitive Closures of Finite Relations
Author: Christian Sternagel (c /dot/ sternagel /at/ gmail /dot/ com) and René Thiemann (rene /dot/ thiemann /at/ uibk /dot/ ac /dot/ at)
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://afp.sf.net/entries/Transitive-Closure.shtml},
             Formal proof development},
   ISSN    = {2150-914x},
 }
License: GNU Lesser General Public License (LGPL)
Depends on:Collections, Abstract-Rewriting
Collections, Matrix

">Proof outline
">Proof document
">Browse theories
">Download this entry
Older releases:
diff --git a/web/entries/Tree-Automata.shtml b/web/entries/Tree-Automata.shtml --- a/web/entries/Tree-Automata.shtml +++ b/web/entries/Tree-Automata.shtml @@ -1,132 +1,132 @@ Archive of Formal Proofs

 

Tree Automata

- +
Title: Tree Automata
Author: Peter Lammich
Submission date: 2009-11-25
Abstract: This work presents a machine-checked tree automata library for Standard-ML, OCaml and Haskell. The algorithms are efficient by using appropriate data structures like RB-trees. The available algorithms for non-deterministic automata include membership query, reduction, intersection, union, and emptiness check with computation of a witness for non-emptiness. The executable algorithms are derived from less-concrete, non-executable algorithms using data-refinement techniques. The concrete data structures are from the Isabelle Collections Framework. Moreover, this work contains a formalization of the class of tree-regular languages and its closure properties under set operations.
BibTeX: 
@article{Tree-Automata-AFP,
   author  = {Peter Lammich},
   title   = {Tree Automata},
   journal = {Archive of Formal Proofs},
   month   = nov,
   year    = 2009,
   note    = {\url{http://afp.sf.net/entries/Tree-Automata.shtml},
             Formal proof development},
   ISSN    = {2150-914x},
 }
License: BSD License
Depends on:Collections
Collections, Automatic_Refinement

">Proof outline
">Proof document
">Browse theories
">Download this entry
Older releases:
diff --git a/web/entries/UpDown_Scheme.shtml b/web/entries/UpDown_Scheme.shtml --- a/web/entries/UpDown_Scheme.shtml +++ b/web/entries/UpDown_Scheme.shtml @@ -1,130 +1,134 @@ Archive of Formal Proofs

 

Verification of the UpDown Scheme

+ + + +
Title: Verification of the UpDown Scheme
Author: Johannes Hölzl (hoelzl /at/ in /dot/ tum /dot/ de)
Submission date: 2015-01-28
Abstract: The UpDown scheme is a recursive scheme used to compute the stiffness matrix on a special form of sparse grids. Usually, when discretizing a Euclidean space of dimension d we need O(n^d) points, for n points along each dimension. Sparse grids are a hierarchical representation where the number of points is reduced to O(n * log(n)^d). One disadvantage of such sparse grids is that the algorithm now operate recursively in the dimensions and levels of the sparse grid.

The UpDown scheme allows us to compute the stiffness matrix on such a sparse grid. The stiffness matrix represents the influence of each representation function on the L^2 scalar product. For a detailed description see Dirk Pflüger's PhD thesis. This formalization was developed as an interdisciplinary project (IDP) at the Technische Universität München.

BibTeX: 
@article{UpDown_Scheme-AFP,
   author  = {Johannes Hölzl},
   title   = {Verification of the UpDown Scheme},
   journal = {Archive of Formal Proofs},
   month   = jan,
   year    = 2015,
   note    = {\url{http://afp.sf.net/entries/UpDown_Scheme.shtml},
             Formal proof development},
   ISSN    = {2150-914x},
 }
License: BSD License
Depends on:Separation_Logic_Imperative_HOL

">Proof outline
">Proof document
">Browse theories
">Download this entry
Older releases:
diff --git a/web/entries/WHATandWHERE_Security.shtml b/web/entries/WHATandWHERE_Security.shtml --- a/web/entries/WHATandWHERE_Security.shtml +++ b/web/entries/WHATandWHERE_Security.shtml @@ -1,146 +1,150 @@ Archive of Formal Proofs

 

A Formalization of Declassification with WHAT-and-WHERE-Security

+ + + +
Title: A Formalization of Declassification with WHAT-and-WHERE-Security
Author: Sylvia Grewe (grewe /at/ cs /dot/ tu-darmstadt /dot/ de), Alexander Lux (lux /at/ mais /dot/ informatik /dot/ tu-darmstadt /dot/ de), Heiko Mantel (mantel /at/ mais /dot/ informatik /dot/ tu-darmstadt /dot/ de) and Jens Sauer (sauer /at/ mais /dot/ informatik /dot/ tu-darmstadt /dot/ de)
Submission date: 2014-04-23
Abstract: Research in information-flow security aims at developing methods to identify undesired information leaks within programs from private sources to public sinks. Noninterference captures this intuition by requiring that no information whatsoever flows from private sources to public sinks. However, in practice this definition is often too strict: Depending on the intuitive desired security policy, the controlled declassification of certain private information (WHAT) at certain points in the program (WHERE) might not result in an undesired information leak.

We present an Isabelle/HOL formalization of such a security property for controlled declassification, namely WHAT&WHERE-security from "Scheduler-Independent Declassification" by Lux, Mantel, and Perner. The formalization includes compositionality proofs for and a soundness proof for a security type system that checks for programs in a simple while language with dynamic thread creation.

Our formalization of the security type system is abstract in the language for expressions and in the semantic side conditions for expressions. It can easily be instantiated with different syntactic approximations for these side conditions. The soundness proof of such an instantiation boils down to showing that these syntactic approximations imply the semantic side conditions.

This Isabelle/HOL formalization uses theories from the entry Strong Security.

BibTeX: 
@article{WHATandWHERE_Security-AFP,
   author  = {Sylvia Grewe and Alexander Lux and Heiko Mantel and Jens Sauer},
   title   = {A Formalization of Declassification with WHAT-and-WHERE-Security},
   journal = {Archive of Formal Proofs},
   month   = apr,
   year    = 2014,
   note    = {\url{http://afp.sf.net/entries/WHATandWHERE_Security.shtml},
             Formal proof development},
   ISSN    = {2150-914x},
 }
License: BSD License
Depends on:Strong_Security

">Proof outline
">Proof document
">Browse theories
">Download this entry
Older releases:
diff --git a/web/entries/Well_Quasi_Orders.shtml b/web/entries/Well_Quasi_Orders.shtml --- a/web/entries/Well_Quasi_Orders.shtml +++ b/web/entries/Well_Quasi_Orders.shtml @@ -1,143 +1,147 @@ Archive of Formal Proofs

 

Well-Quasi-Orders

+ + + +
Title: Well-Quasi-Orders
Author: 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.
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://afp.sf.net/entries/Well_Quasi_Orders.shtml},
             Formal proof development},
   ISSN    = {2150-914x},
 }
License: BSD License
Depends on:Abstract-Rewriting, Regular-Sets, Open_Induction

">Proof outline
">Proof document
">Browse theories
">Download this entry
Older releases:
diff --git a/web/entries/XML.shtml b/web/entries/XML.shtml --- a/web/entries/XML.shtml +++ b/web/entries/XML.shtml @@ -1,125 +1,125 @@ Archive of Formal Proofs

 

XML

- +
Title: XML
Author: Christian Sternagel (c /dot/ sternagel /at/ gmail /dot/ com) and René Thiemann (rene /dot/ thiemann /at/ uibk /dot/ ac /dot/ at)
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://afp.sf.net/entries/XML.shtml},
             Formal proof development},
   ISSN    = {2150-914x},
 }
License: BSD License
Depends on:Show, Partial_Function_MR, Certification_Monads
Certification_Monads, Partial_Function_MR, Show

">Proof outline
">Proof document
">Browse theories
">Download this entry
Older releases: