diff --git a/admin/site/content/about.md b/admin/site/content/about.md
--- a/admin/site/content/about.md
+++ b/admin/site/content/about.md
@@ -1,54 +1,58 @@
---
title: "About"
-menu:
+menu:
main:
name: "About"
weight: 7
---
The Archive of Formal Proofs is a collection of proof libraries, examples, and larger scientific developments,
mechanically checked in the theorem prover Isabelle.
It is organized in the way of a scientific journal.
[Submissions](/submission) are refereed.
The archive repository is hosted on [Heptapod](https://foss.heptapod.net/isa-afp/) to provide easy free access to archive entries.
The entries are tested and maintained continuously against the current stable release of Isabelle.
Older versions of archive entries will remain available.
## Editors
The editors of the Archive of Formal Proofs are:
-* [Manuel Eberl](https://www.in.tum.de/~eberlm/), [Technische Universität München](https://www.tum.de/)
-* [Gerwin Klein](https://www.cse.unsw.edu.au/~kleing/), [Data61](https://www.data61.csiro.au)
-* [Tobias Nipkow](https://www.in.tum.de/~nipkow/), [Technische Universität München](https://www.tum.de/)
-* [Larry Paulson](https://www.cl.cam.ac.uk/users/lcp/), [University of Cambridge](https://www.cam.ac.uk/)
-* [René Thiemann](http://cl-informatik.uibk.ac.at/users/thiemann/), [University of Innsbruck](https://www.uibk.ac.at/)
+* [Manuel Eberl](http://pruvisto.org/), [University of Innsbruck](https://www.uibk.ac.at/)
+* [Gerwin Klein](https://www.cse.unsw.edu.au/~kleing/), [Proofcraft](https://proofcraft.systems) & [UNSW Sydney](https://www.unsw.edu.au/)
+* [Andreas Lochbihler](http://www.andreas-lochbihler.de),
+ [Digital Asset](https://www.digitalasset.com)
+* [Tobias Nipkow](https://www.in.tum.de/~nipkow/), [Technische Universität München](https://www.tum.de/)
+* [Larry Paulson](https://www.cl.cam.ac.uk/users/lcp/), [University of Cambridge](https://www.cam.ac.uk/)
+* [René Thiemann](http://cl-informatik.uibk.ac.at/users/thiemann/), [University of Innsbruck](https://www.uibk.ac.at/)
## Why
We aim to strengthen the community and to foster the development of formal proofs.
We hope that the Archive will provide:
-* a resource of knowledge, examples, and libraries for users,
-* a large and relevant test bed of theories for Isabelle developers, and
-* a central, citable place for authors to publish their theories
+* a resource of knowledge, examples, and libraries for users,
+* a large and relevant test bed of theories for Isabelle developers, and
+* a central, citable place for authors to publish their theories
We encourage authors of publications that contain Isabelle developments to make their theories available in the Archive of Formal Proofs and to refer to the archive entry in their publication. It makes it easier for referees to check the validity of theorems (all entries in the Archive are mechanically checked), it makes it easier for readers of the publication to understand details of your development, and it makes it easier to use and build on your work.
## License
All entries in the Archive of Formal Proofs are licensed under a [BSD-style License](LICENSE) or the [GNU LGPL](https://www.gnu.org/copyleft/lesser.html). This means they are free to download, free to use, free to change, and free to redistribute with minimal restrictions.
The authors retain their full copyright on their original work, including their right to make the development available under another, additional license in the future.
## Website
This website is the result of a project from the School of Informatics at the [University of Edinburgh](https://www.ed.ac.uk) by:
- * Carlin MacKenzie, [AIML](https://aiml.inf.ed.ac.uk)
- * James Vaughan, [AIAI](https://web.inf.ed.ac.uk/aiai/)
- * Jacques Fleuriot, [AIAI](https://web.inf.ed.ac.uk/aiai/)
+
+* Carlin MacKenzie, [AIML](https://aiml.inf.ed.ac.uk)
+* James Vaughan, [AIAI](https://web.inf.ed.ac.uk/aiai/)
+* Jacques Fleuriot, [AIAI](https://web.inf.ed.ac.uk/aiai/)
Integration and maintenance by:
- * [Fabian Huch](https://www21.in.tum.de/team/huch), [Technische Universität München](https://www.tum.de/)
+
+* [Fabian Huch](https://www21.in.tum.de/team/huch), [Technische Universität München](https://www.tum.de/)
diff --git a/admin/site/content/help.md b/admin/site/content/help.md
--- a/admin/site/content/help.md
+++ b/admin/site/content/help.md
@@ -1,62 +1,62 @@
---
title: Help
-menu:
+menu:
main:
name: "Help"
weight: 4
---
This section focuses on the Archive of Formal Proofs. For help with Isabelle, see the [Isabelle Wiki](https://isabelle.in.tum.de/community/Main_Page) and [Documentation](https://isabelle.in.tum.de/documentation.html)
## Referring to AFP Entries in Isabelle/JEdit
Once you have downloaded the AFP, you can include its articles and theories in your own developments. If you would like to make your work available to others _without_ having to include the AFP articles you depend on, here is how to do it.
-From Isabelle2021 on, the recommended method for making the whole AFP available to Isabelle is the `isabelle components -u` command.
+From Isabelle2021-1 on, the recommended method for making the whole AFP available to Isabelle is the `isabelle components -u` command.
#### Linux and Mac
Assuming you have downloaded and unzipped the afp to `/home/myself/afp`, run:
- isabelle components -u /home/myself/afp
+ isabelle components -u /home/myself/afp/thys
#### Windows
If the AFP is in `C:\afp`, run the following command in a Cygwin terminal:
- isabelle components -u /cygdrive/c/afp
+ isabelle components -u /cygdrive/c/afp/thys
#### Use
You can now refer to article `ABC` from the AFP in another theory via:
imports "ABC.Some_ABC_Theory"
This allows you to distribute your material separately from any AFP theories. Users of your distribution also need to install the AFP in the above manner.
## Citing Entries
The following gives an example of the preferred way for citing entries in the AFP:
> M. Jaskelioff and S. Merz, Proving the Correctness of Disk Paxos. _Archive of Formal Proofs_, June 2005, [https://isa-afp.org/entries/DiskPaxos.html](https://isa-afp.org/entries/DiskPaxos.html), Formal proof development.
-The bibtext entry for this would be:
+The bibtex entry for this would be:
```
@article{Jaskelioff-Merz-AFP05,
author = {Mauro Jaskelioff and Stephan Merz},
title = {Proving the Correctness of Disk Paxos},
journal = {Archive of Formal Proofs},
month = Jun,
year = 2005,
note = {\\url{https://isa-afp.org/entries/DiskPaxos.html}, Formal proof development},
ISSN = {2150-914x}
}
```
## Mailing Lists
* isabelle-users@cl.cam.ac.uk provides a forum for Isabelle users to discuss problems, exchange information, and make announcements. Users of official Isabelle releases should subscribe or see the archive.
-
+
* isabelle-dev@in.tum.de covers the Isabelle development process, including intermediate repository versions, and administrative issues concerning the website or testing infrastructure. Early adopters of development snapshots or repository versions should subscribe or see the archive (also available at mail-archive.com).
diff --git a/web/about/index.html b/web/about/index.html
--- a/web/about/index.html
+++ b/web/about/index.html
@@ -1,126 +1,128 @@
About - Archive of Formal Proofs
About
The Archive of Formal Proofs is a collection of proof libraries, examples, and larger scientific developments,
mechanically checked in the theorem prover Isabelle.
It is organized in the way of a scientific journal.
Submissions are refereed.
The archive repository is hosted on Heptapod to provide easy free access to archive entries.
The entries are tested and maintained continuously against the current stable release of Isabelle.
Older versions of archive entries will remain available.
We aim to strengthen the community and to foster the development of formal proofs.
We hope that the Archive will provide:
a resource of knowledge, examples, and libraries for users,
a large and relevant test bed of theories for Isabelle developers, and
a central, citable place for authors to publish their theories
We encourage authors of publications that contain Isabelle developments to make their theories available in the Archive of Formal Proofs and to refer to the archive entry in their publication. It makes it easier for referees to check the validity of theorems (all entries in the Archive are mechanically checked), it makes it easier for readers of the publication to understand details of your development, and it makes it easier to use and build on your work.
License
All entries in the Archive of Formal Proofs are licensed under a BSD-style License or the GNU LGPL. This means they are free to download, free to use, free to change, and free to redistribute with minimal restrictions.
The authors retain their full copyright on their original work, including their right to make the development available under another, additional license in the future.
Website
This website is the result of a project from the School of Informatics at the University of Edinburgh by:
\ No newline at end of file
diff --git a/web/help/index.html b/web/help/index.html
--- a/web/help/index.html
+++ b/web/help/index.html
@@ -1,130 +1,130 @@
Help - Archive of Formal Proofs
+From Isabelle2021-1 on, the recommended method for making the whole AFP available to Isabelle is the isabelle components -u command." />
+From Isabelle2021-1 on, the recommended method for making the whole AFP available to Isabelle is the isabelle components -u command."/>
Help
This section focuses on the Archive of Formal Proofs. For help with Isabelle, see the Isabelle Wiki and Documentation
Referring to AFP Entries in Isabelle/JEdit
Once you have downloaded the AFP, you can include its articles and theories in your own developments. If you would like to make your work available to others without having to include the AFP articles you depend on, here is how to do it.
-
From Isabelle2021 on, the recommended method for making the whole AFP available to Isabelle is the isabelle components -u command.
+
From Isabelle2021-1 on, the recommended method for making the whole AFP available to Isabelle is the isabelle components -u command.
Linux and Mac
Assuming you have downloaded and unzipped the afp to /home/myself/afp, run:
-
isabelle components -u /home/myself/afp
+
isabelle components -u /home/myself/afp/thys
Windows
If the AFP is in C:\afp, run the following command in a Cygwin terminal:
-
isabelle components -u /cygdrive/c/afp
+
isabelle components -u /cygdrive/c/afp/thys
Use
You can now refer to article ABC from the AFP in another theory via:
imports "ABC.Some_ABC_Theory"
This allows you to distribute your material separately from any AFP theories. Users of your distribution also need to install the AFP in the above manner.
Citing Entries
The following gives an example of the preferred way for citing entries in the AFP:
M. Jaskelioff and S. Merz, Proving the Correctness of Disk Paxos. Archive of Formal Proofs, June 2005, https://isa-afp.org/entries/DiskPaxos.html, Formal proof development.
-
The bibtext entry for this would be:
+
The bibtex entry for this would be:
@article{Jaskelioff-Merz-AFP05,
author = {Mauro Jaskelioff and Stephan Merz},
title = {Proving the Correctness of Disk Paxos},
journal = {Archive of Formal Proofs},
month = Jun,
year = 2005,
note = {\\url{https://isa-afp.org/entries/DiskPaxos.html}, Formal proof development},
ISSN = {2150-914x}
}
Mailing Lists
isabelle-users@cl.cam.ac.uk provides a forum for Isabelle users to discuss problems, exchange information, and make announcements. Users of official Isabelle releases should subscribe or see the archive.
isabelle-dev@in.tum.de covers the Isabelle development process, including intermediate repository versions, and administrative issues concerning the website or testing infrastructure. Early adopters of development snapshots or repository versions should subscribe or see the archive (also available at mail-archive.com).
\ No newline at end of file
diff --git a/web/index.xml b/web/index.xml
--- a/web/index.xml
+++ b/web/index.xml
@@ -1,12610 +1,12610 @@
Archive of Formal Proofs
/
Recent content on Archive of Formal ProofsHugo -- gohugo.ioen-gbWed, 08 Jun 2022 00:00:00 +0000Finite Fields
/entries/Finite_Fields.html
Wed, 08 Jun 2022 00:00:00 +0000/entries/Finite_Fields.htmlDiophantine Equations and the DPRM Theorem
/entries/DPRM_Theorem.html
Mon, 06 Jun 2022 00:00:00 +0000/entries/DPRM_Theorem.htmlReducing Rewrite Properties to Properties on Ground Terms
/entries/Rewrite_Properties_Reduction.html
Thu, 02 Jun 2022 00:00:00 +0000/entries/Rewrite_Properties_Reduction.htmlA Restricted Definition of the Magic Wand to Soundly Combine Fractions of a Wand
/entries/Combinable_Wands.html
Mon, 30 May 2022 00:00:00 +0000/entries/Combinable_Wands.htmlThe Plünnecke-Ruzsa Inequality
/entries/Pluennecke_Ruzsa_Inequality.html
Thu, 26 May 2022 00:00:00 +0000/entries/Pluennecke_Ruzsa_Inequality.htmlFormalization of a Framework for the Sound Automation of Magic Wands
/entries/Package_logic.html
Wed, 18 May 2022 00:00:00 +0000/entries/Package_logic.htmlClique is not solvable by monotone circuits of polynomial size
/entries/Clique_and_Monotone_Circuits.html
Sun, 08 May 2022 00:00:00 +0000/entries/Clique_and_Monotone_Circuits.htmlFisher's Inequality: Linear Algebraic Proof Techniques for Combinatorics
/entries/Fishers_Inequality.html
Thu, 21 Apr 2022 00:00:00 +0000/entries/Fishers_Inequality.htmlDigit Expansions
/entries/Digit_Expansions.html
Wed, 20 Apr 2022 00:00:00 +0000/entries/Digit_Expansions.htmlThe Generalized Multiset Ordering is NP-Complete
/entries/Multiset_Ordering_NPC.html
Wed, 20 Apr 2022 00:00:00 +0000/entries/Multiset_Ordering_NPC.htmlThe Sophomore's Dream
/entries/Sophomores_Dream.html
Sun, 10 Apr 2022 00:00:00 +0000/entries/Sophomores_Dream.htmlA Combinator Library for Prefix-Free Codes
/entries/Prefix_Free_Code_Combinators.html
Fri, 08 Apr 2022 00:00:00 +0000/entries/Prefix_Free_Code_Combinators.htmlFormalization of Randomized Approximation Algorithms for Frequency Moments
/entries/Frequency_Moments.html
Fri, 08 Apr 2022 00:00:00 +0000/entries/Frequency_Moments.htmlConstructing the Reals as Dedekind Cuts of Rationals
/entries/Dedekind_Real.html
Thu, 24 Mar 2022 00:00:00 +0000/entries/Dedekind_Real.htmlAckermann's Function Is Not Primitive Recursive
/entries/Ackermanns_not_PR.html
Wed, 23 Mar 2022 00:00:00 +0000/entries/Ackermanns_not_PR.htmlA Naive Prover for First-Order Logic
/entries/FOL_Seq_Calc3.html
Tue, 22 Mar 2022 00:00:00 +0000/entries/FOL_Seq_Calc3.htmlA Proof from THE BOOK: The Partial Fraction Expansion of the Cotangent
/entries/Cotangent_PFD_Formula.html
Tue, 15 Mar 2022 00:00:00 +0000/entries/Cotangent_PFD_Formula.htmlThe Independence of the Continuum Hypothesis in Isabelle/ZF
/entries/Independence_CH.html
Sun, 06 Mar 2022 00:00:00 +0000/entries/Independence_CH.htmlTransitive Models of Fragments of ZFC
/entries/Transitive_Models.html
Thu, 03 Mar 2022 00:00:00 +0000/entries/Transitive_Models.htmlResiduated Transition Systems
/entries/ResiduatedTransitionSystem.html
Mon, 28 Feb 2022 00:00:00 +0000/entries/ResiduatedTransitionSystem.htmlUniversal Hash Families
/entries/Universal_Hash_Families.html
Sun, 20 Feb 2022 00:00:00 +0000/entries/Universal_Hash_Families.htmlWetzel's Problem and the Continuum Hypothesis
/entries/Wetzels_Problem.html
Fri, 18 Feb 2022 00:00:00 +0000/entries/Wetzels_Problem.htmlFirst-Order Query Evaluation
/entries/Eval_FO.html
Tue, 15 Feb 2022 00:00:00 +0000/entries/Eval_FO.htmlMulti-Head Monitoring of Metric Dynamic Logic
/entries/VYDRA_MDL.html
Sun, 13 Feb 2022 00:00:00 +0000/entries/VYDRA_MDL.htmlEnumeration of Equivalence Relations
/entries/Equivalence_Relation_Enumeration.html
Fri, 04 Feb 2022 00:00:00 +0000/entries/Equivalence_Relation_Enumeration.htmlDuality of Linear Programming
/entries/LP_Duality.html
Thu, 03 Feb 2022 00:00:00 +0000/entries/LP_Duality.htmlQuasi-Borel Spaces
/entries/Quasi_Borel_Spaces.html
Thu, 03 Feb 2022 00:00:00 +0000/entries/Quasi_Borel_Spaces.htmlFirst-Order Theory of Rewriting
/entries/FO_Theory_Rewriting.html
Wed, 02 Feb 2022 00:00:00 +0000/entries/FO_Theory_Rewriting.htmlA Sequent Calculus Prover for First-Order Logic with Functions
/entries/FOL_Seq_Calc2.html
Mon, 31 Jan 2022 00:00:00 +0000/entries/FOL_Seq_Calc2.htmlYoung's Inequality for Increasing Functions
/entries/Youngs_Inequality.html
Mon, 31 Jan 2022 00:00:00 +0000/entries/Youngs_Inequality.htmlInterpolation Polynomials (in HOL-Algebra)
/entries/Interpolation_Polynomials_HOL_Algebra.html
Sat, 29 Jan 2022 00:00:00 +0000/entries/Interpolation_Polynomials_HOL_Algebra.htmlMedian Method
/entries/Median_Method.html
Tue, 25 Jan 2022 00:00:00 +0000/entries/Median_Method.htmlActuarial Mathematics
/entries/Actuarial_Mathematics.html
Sun, 23 Jan 2022 00:00:00 +0000/entries/Actuarial_Mathematics.htmlIrrational numbers from THE BOOK
/entries/Irrationals_From_THEBOOK.html
Sat, 08 Jan 2022 00:00:00 +0000/entries/Irrationals_From_THEBOOK.htmlKnight's Tour Revisited Revisited
/entries/Knights_Tour.html
Tue, 04 Jan 2022 00:00:00 +0000/entries/Knights_Tour.htmlHyperdual Numbers and Forward Differentiation
/entries/Hyperdual.html
Fri, 31 Dec 2021 00:00:00 +0000/entries/Hyperdual.htmlGale-Shapley Algorithm
/entries/Gale_Shapley.html
Wed, 29 Dec 2021 00:00:00 +0000/entries/Gale_Shapley.htmlRoth's Theorem on Arithmetic Progressions
/entries/Roth_Arithmetic_Progressions.html
Tue, 28 Dec 2021 00:00:00 +0000/entries/Roth_Arithmetic_Progressions.htmlMarkov Decision Processes with Rewards
/entries/MDP-Rewards.html
Thu, 16 Dec 2021 00:00:00 +0000/entries/MDP-Rewards.htmlVerified Algorithms for Solving Markov Decision Processes
/entries/MDP-Algorithms.html
Thu, 16 Dec 2021 00:00:00 +0000/entries/MDP-Algorithms.htmlRegular Tree Relations
/entries/Regular_Tree_Relations.html
Wed, 15 Dec 2021 00:00:00 +0000/entries/Regular_Tree_Relations.htmlSimplicial Complexes and Boolean functions
/entries/Simplicial_complexes_and_boolean_functions.html
Mon, 29 Nov 2021 00:00:00 +0000/entries/Simplicial_complexes_and_boolean_functions.htmlvan Emde Boas Trees
/entries/Van_Emde_Boas_Trees.html
Tue, 23 Nov 2021 00:00:00 +0000/entries/Van_Emde_Boas_Trees.htmlFoundation of geometry in planes, and some complements: Excluding the parallel axioms
/entries/Foundation_of_geometry.html
Mon, 22 Nov 2021 00:00:00 +0000/entries/Foundation_of_geometry.htmlThe Hahn and Jordan Decomposition Theorems
/entries/Hahn_Jordan_Decomposition.html
Fri, 19 Nov 2021 00:00:00 +0000/entries/Hahn_Jordan_Decomposition.htmlAutomating Public Announcement Logic and the Wise Men Puzzle in Isabelle/HOL
/entries/PAL.html
Mon, 08 Nov 2021 00:00:00 +0000/entries/PAL.htmlExploring Simplified Variants of Gödel’s Ontological Argument in Isabelle/HOL
/entries/SimplifiedOntologicalArgument.html
Mon, 08 Nov 2021 00:00:00 +0000/entries/SimplifiedOntologicalArgument.htmlFactorization of Polynomials with Algebraic Coefficients
/entries/Factor_Algebraic_Polynomial.html
Mon, 08 Nov 2021 00:00:00 +0000/entries/Factor_Algebraic_Polynomial.htmlReal Exponents as the Limits of Sequences of Rational Exponents
/entries/Real_Power.html
Mon, 08 Nov 2021 00:00:00 +0000/entries/Real_Power.htmlSzemerédi's Regularity Lemma
/entries/Szemeredi_Regularity.html
Fri, 05 Nov 2021 00:00:00 +0000/entries/Szemeredi_Regularity.htmlQuantum and Classical Registers
/entries/Registers.html
Thu, 28 Oct 2021 00:00:00 +0000/entries/Registers.htmlBelief Revision Theory
/entries/Belief_Revision.html
Tue, 19 Oct 2021 00:00:00 +0000/entries/Belief_Revision.htmlX86 instruction semantics and basic block symbolic execution
/entries/X86_Semantics.html
Wed, 13 Oct 2021 00:00:00 +0000/entries/X86_Semantics.htmlAlgebras for Iteration, Infinite Executions and Correctness of Sequential Computations
/entries/Correctness_Algebras.html
Tue, 12 Oct 2021 00:00:00 +0000/entries/Correctness_Algebras.htmlVerified Quadratic Virtual Substitution for Real Arithmetic
/entries/Virtual_Substitution.html
Sat, 02 Oct 2021 00:00:00 +0000/entries/Virtual_Substitution.htmlSoundness and Completeness of an Axiomatic System for First-Order Logic
/entries/FOL_Axiomatic.html
Fri, 24 Sep 2021 00:00:00 +0000/entries/FOL_Axiomatic.htmlComplex Bounded Operators
/entries/Complex_Bounded_Operators.html
Sat, 18 Sep 2021 00:00:00 +0000/entries/Complex_Bounded_Operators.htmlA Formalization of Weighted Path Orders and Recursive Path Orders
/entries/Weighted_Path_Order.html
Thu, 16 Sep 2021 00:00:00 +0000/entries/Weighted_Path_Order.htmlCategory Theory for ZFC in HOL I: Foundations: Design Patterns, Set Theory, Digraphs, Semicategories
/entries/CZH_Foundations.html
Mon, 06 Sep 2021 00:00:00 +0000/entries/CZH_Foundations.htmlCategory Theory for ZFC in HOL II: Elementary Theory of 1-Categories
/entries/CZH_Elementary_Categories.html
Mon, 06 Sep 2021 00:00:00 +0000/entries/CZH_Elementary_Categories.htmlCategory Theory for ZFC in HOL III: Universal Constructions
/entries/CZH_Universal_Constructions.html
Mon, 06 Sep 2021 00:00:00 +0000/entries/CZH_Universal_Constructions.htmlConditional Simplification
/entries/Conditional_Simplification.html
Mon, 06 Sep 2021 00:00:00 +0000/entries/Conditional_Simplification.htmlConditional Transfer Rule
/entries/Conditional_Transfer_Rule.html
Mon, 06 Sep 2021 00:00:00 +0000/entries/Conditional_Transfer_Rule.htmlExtension of Types-To-Sets
/entries/Types_To_Sets_Extension.html
Mon, 06 Sep 2021 00:00:00 +0000/entries/Types_To_Sets_Extension.htmlIDE: Introduction, Destruction, Elimination
/entries/Intro_Dest_Elim.html
Mon, 06 Sep 2021 00:00:00 +0000/entries/Intro_Dest_Elim.htmlA data flow analysis algorithm for computing dominators
/entries/Dominance_CHK.html
Sun, 05 Sep 2021 00:00:00 +0000/entries/Dominance_CHK.htmlSolving Cubic and Quartic Equations
/entries/Cubic_Quartic_Equations.html
Fri, 03 Sep 2021 00:00:00 +0000/entries/Cubic_Quartic_Equations.htmlLogging-independent Message Anonymity in the Relational Method
/entries/Logging_Independent_Anonymity.html
Thu, 26 Aug 2021 00:00:00 +0000/entries/Logging_Independent_Anonymity.htmlThe Theorem of Three Circles
/entries/Three_Circles.html
Sat, 21 Aug 2021 00:00:00 +0000/entries/Three_Circles.htmlCoCon: A Confidentiality-Verified Conference Management System
/entries/CoCon.html
Mon, 16 Aug 2021 00:00:00 +0000/entries/CoCon.htmlCompositional BD Security
/entries/BD_Security_Compositional.html
Mon, 16 Aug 2021 00:00:00 +0000/entries/BD_Security_Compositional.htmlCoSMed: A confidentiality-verified social media platform
/entries/CoSMed.html
Mon, 16 Aug 2021 00:00:00 +0000/entries/CoSMed.htmlCoSMeDis: A confidentiality-verified distributed social media platform
/entries/CoSMeDis.html
Mon, 16 Aug 2021 00:00:00 +0000/entries/CoSMeDis.htmlFresh identifiers
/entries/Fresh_Identifiers.html
Mon, 16 Aug 2021 00:00:00 +0000/entries/Fresh_Identifiers.htmlCombinatorial Design Theory
/entries/Design_Theory.html
Fri, 13 Aug 2021 00:00:00 +0000/entries/Design_Theory.htmlRelational Forests
/entries/Relational_Forests.html
Tue, 03 Aug 2021 00:00:00 +0000/entries/Relational_Forests.htmlSchutz' Independent Axioms for Minkowski Spacetime
/entries/Schutz_Spacetime.html
Tue, 27 Jul 2021 00:00:00 +0000/entries/Schutz_Spacetime.htmlFinitely Generated Abelian Groups
/entries/Finitely_Generated_Abelian_Groups.html
Wed, 07 Jul 2021 00:00:00 +0000/entries/Finitely_Generated_Abelian_Groups.htmlSpecCheck - Specification-Based Testing for Isabelle/ML
/entries/SpecCheck.html
Thu, 01 Jul 2021 00:00:00 +0000/entries/SpecCheck.htmlVan der Waerden's Theorem
/entries/Van_der_Waerden.html
Tue, 22 Jun 2021 00:00:00 +0000/entries/Van_der_Waerden.htmlMiniSail - A kernel language for the ISA specification language SAIL
/entries/MiniSail.html
Fri, 18 Jun 2021 00:00:00 +0000/entries/MiniSail.htmlPublic Announcement Logic
/entries/Public_Announcement_Logic.html
Thu, 17 Jun 2021 00:00:00 +0000/entries/Public_Announcement_Logic.htmlA Shorter Compiler Correctness Proof for Language IMP
/entries/IMP_Compiler.html
Fri, 04 Jun 2021 00:00:00 +0000/entries/IMP_Compiler.htmlCombinatorics on Words Basics
/entries/Combinatorics_Words.html
Mon, 24 May 2021 00:00:00 +0000/entries/Combinatorics_Words.htmlGraph Lemma
/entries/Combinatorics_Words_Graph_Lemma.html
Mon, 24 May 2021 00:00:00 +0000/entries/Combinatorics_Words_Graph_Lemma.htmlLyndon words
/entries/Combinatorics_Words_Lyndon.html
Mon, 24 May 2021 00:00:00 +0000/entries/Combinatorics_Words_Lyndon.htmlRegression Test Selection
/entries/Regression_Test_Selection.html
Fri, 30 Apr 2021 00:00:00 +0000/entries/Regression_Test_Selection.htmlIsabelle's Metalogic: Formalization and Proof Checker
/entries/Metalogic_ProofChecker.html
Tue, 27 Apr 2021 00:00:00 +0000/entries/Metalogic_ProofChecker.htmlLifting the Exponent
/entries/Lifting_the_Exponent.html
Tue, 27 Apr 2021 00:00:00 +0000/entries/Lifting_the_Exponent.htmlThe BKR Decision Procedure for Univariate Real Arithmetic
/entries/BenOr_Kozen_Reif.html
Sat, 24 Apr 2021 00:00:00 +0000/entries/BenOr_Kozen_Reif.htmlGale-Stewart Games
/entries/GaleStewart_Games.html
Fri, 23 Apr 2021 00:00:00 +0000/entries/GaleStewart_Games.htmlFormalization of Timely Dataflow's Progress Tracking Protocol
/entries/Progress_Tracking.html
Tue, 13 Apr 2021 00:00:00 +0000/entries/Progress_Tracking.htmlInformation Flow Control via Dependency Tracking
/entries/IFC_Tracking.html
Thu, 01 Apr 2021 00:00:00 +0000/entries/IFC_Tracking.htmlGrothendieck's Schemes in Algebraic Geometry
/entries/Grothendieck_Schemes.html
Mon, 29 Mar 2021 00:00:00 +0000/entries/Grothendieck_Schemes.htmlHensel's Lemma for the p-adic Integers
/entries/Padic_Ints.html
Tue, 23 Mar 2021 00:00:00 +0000/entries/Padic_Ints.htmlConstructive Cryptography in HOL: the Communication Modeling Aspect
/entries/Constructive_Cryptography_CM.html
Wed, 17 Mar 2021 00:00:00 +0000/entries/Constructive_Cryptography_CM.htmlTwo algorithms based on modular arithmetic: lattice basis reduction and Hermite normal form computation
/entries/Modular_arithmetic_LLL_and_HNF_algorithms.html
Fri, 12 Mar 2021 00:00:00 +0000/entries/Modular_arithmetic_LLL_and_HNF_algorithms.htmlQuantum projective measurements and the CHSH inequality
/entries/Projective_Measurements.html
Wed, 03 Mar 2021 00:00:00 +0000/entries/Projective_Measurements.htmlThe Hermite–Lindemann–Weierstraß Transcendence Theorem
/entries/Hermite_Lindemann.html
Wed, 03 Mar 2021 00:00:00 +0000/entries/Hermite_Lindemann.htmlMereology
/entries/Mereology.html
Mon, 01 Mar 2021 00:00:00 +0000/entries/Mereology.htmlThe Sunflower Lemma of Erdős and Rado
/entries/Sunflowers.html
Thu, 25 Feb 2021 00:00:00 +0000/entries/Sunflowers.htmlA Verified Imperative Implementation of B-Trees
/entries/BTree.html
Wed, 24 Feb 2021 00:00:00 +0000/entries/BTree.htmlFormal Puiseux Series
/entries/Formal_Puiseux_Series.html
Wed, 17 Feb 2021 00:00:00 +0000/entries/Formal_Puiseux_Series.htmlThe Laws of Large Numbers
/entries/Laws_of_Large_Numbers.html
Wed, 10 Feb 2021 00:00:00 +0000/entries/Laws_of_Large_Numbers.htmlTarski's Parallel Postulate implies the 5th Postulate of Euclid, the Postulate of Playfair and the original Parallel Postulate of Euclid
/entries/IsaGeoCoq.html
Sun, 31 Jan 2021 00:00:00 +0000/entries/IsaGeoCoq.htmlSolution to the xkcd Blue Eyes puzzle
/entries/Blue_Eyes.html
Sat, 30 Jan 2021 00:00:00 +0000/entries/Blue_Eyes.htmlHood-Melville Queue
/entries/Hood_Melville_Queue.html
Mon, 18 Jan 2021 00:00:00 +0000/entries/Hood_Melville_Queue.htmlJinjaDCI: a Java semantics with dynamic class initialization
/entries/JinjaDCI.html
Mon, 11 Jan 2021 00:00:00 +0000/entries/JinjaDCI.htmlCofinality and the Delta System Lemma
/entries/Delta_System_Lemma.html
Sun, 27 Dec 2020 00:00:00 +0000/entries/Delta_System_Lemma.htmlTopological semantics for paraconsistent and paracomplete logics
/entries/Topological_Semantics.html
Thu, 17 Dec 2020 00:00:00 +0000/entries/Topological_Semantics.htmlRelational Minimum Spanning Tree Algorithms
/entries/Relational_Minimum_Spanning_Trees.html
Tue, 08 Dec 2020 00:00:00 +0000/entries/Relational_Minimum_Spanning_Trees.htmlInline Caching and Unboxing Optimization for Interpreters
/entries/Interpreter_Optimizations.html
Mon, 07 Dec 2020 00:00:00 +0000/entries/Interpreter_Optimizations.htmlThe Relational Method with Message Anonymity for the Verification of Cryptographic Protocols
/entries/Relational_Method.html
Sat, 05 Dec 2020 00:00:00 +0000/entries/Relational_Method.htmlIsabelle Marries Dirac: a Library for Quantum Computation and Quantum Information
/entries/Isabelle_Marries_Dirac.html
Sun, 22 Nov 2020 00:00:00 +0000/entries/Isabelle_Marries_Dirac.htmlThe HOL-CSP Refinement Toolkit
/entries/CSP_RefTK.html
Thu, 19 Nov 2020 00:00:00 +0000/entries/CSP_RefTK.htmlAI Planning Languages Semantics
/entries/AI_Planning_Languages_Semantics.html
Thu, 29 Oct 2020 00:00:00 +0000/entries/AI_Planning_Languages_Semantics.htmlVerified SAT-Based AI Planning
/entries/Verified_SAT_Based_AI_Planning.html
Thu, 29 Oct 2020 00:00:00 +0000/entries/Verified_SAT_Based_AI_Planning.htmlA Sound Type System for Physical Quantities, Units, and Measurements
/entries/Physical_Quantities.html
Tue, 20 Oct 2020 00:00:00 +0000/entries/Physical_Quantities.htmlFinite Map Extras
/entries/Finite-Map-Extras.html
Mon, 12 Oct 2020 00:00:00 +0000/entries/Finite-Map-Extras.htmlA Formal Model of the Document Object Model with Shadow Roots
/entries/Shadow_DOM.html
Mon, 28 Sep 2020 00:00:00 +0000/entries/Shadow_DOM.htmlA Formal Model of the Safely Composable Document Object Model with Shadow Roots
/entries/Shadow_SC_DOM.html
Mon, 28 Sep 2020 00:00:00 +0000/entries/Shadow_SC_DOM.htmlA Formalization of Safely Composable Web Components
/entries/SC_DOM_Components.html
Mon, 28 Sep 2020 00:00:00 +0000/entries/SC_DOM_Components.htmlA Formalization of Web Components
/entries/DOM_Components.html
Mon, 28 Sep 2020 00:00:00 +0000/entries/DOM_Components.htmlThe Safely Composable DOM
/entries/Core_SC_DOM.html
Mon, 28 Sep 2020 00:00:00 +0000/entries/Core_SC_DOM.htmlAn Abstract Formalization of Gödel's Incompleteness Theorems
/entries/Goedel_Incompleteness.html
Wed, 16 Sep 2020 00:00:00 +0000/entries/Goedel_Incompleteness.htmlFrom Abstract to Concrete Gödel's Incompleteness Theorems—Part I
/entries/Goedel_HFSet_Semantic.html
Wed, 16 Sep 2020 00:00:00 +0000/entries/Goedel_HFSet_Semantic.htmlFrom Abstract to Concrete Gödel's Incompleteness Theorems—Part II
/entries/Goedel_HFSet_Semanticless.html
Wed, 16 Sep 2020 00:00:00 +0000/entries/Goedel_HFSet_Semanticless.htmlRobinson Arithmetic
/entries/Robinson_Arithmetic.html
Wed, 16 Sep 2020 00:00:00 +0000/entries/Robinson_Arithmetic.htmlSyntax-Independent Logic Infrastructure
/entries/Syntax_Independent_Logic.html
Wed, 16 Sep 2020 00:00:00 +0000/entries/Syntax_Independent_Logic.htmlA Formal Model of Extended Finite State Machines
/entries/Extended_Finite_State_Machines.html
Mon, 07 Sep 2020 00:00:00 +0000/entries/Extended_Finite_State_Machines.htmlInference of Extended Finite State Machines
/entries/Extended_Finite_State_Machine_Inference.html
Mon, 07 Sep 2020 00:00:00 +0000/entries/Extended_Finite_State_Machine_Inference.htmlPractical Algebraic Calculus Checker
/entries/PAC_Checker.html
Mon, 31 Aug 2020 00:00:00 +0000/entries/PAC_Checker.htmlSome classical results in inductive inference of recursive functions
/entries/Inductive_Inference.html
Mon, 31 Aug 2020 00:00:00 +0000/entries/Inductive_Inference.htmlRelational Disjoint-Set Forests
/entries/Relational_Disjoint_Set_Forests.html
Wed, 26 Aug 2020 00:00:00 +0000/entries/Relational_Disjoint_Set_Forests.htmlExtensions to the Comprehensive Framework for Saturation Theorem Proving
/entries/Saturation_Framework_Extensions.html
Tue, 25 Aug 2020 00:00:00 +0000/entries/Saturation_Framework_Extensions.htmlPutting the `K' into Bird's derivation of Knuth-Morris-Pratt string matching
/entries/BirdKMP.html
Tue, 25 Aug 2020 00:00:00 +0000/entries/BirdKMP.htmlAmicable Numbers
/entries/Amicable_Numbers.html
Tue, 04 Aug 2020 00:00:00 +0000/entries/Amicable_Numbers.htmlOrdinal Partitions
/entries/Ordinal_Partitions.html
Mon, 03 Aug 2020 00:00:00 +0000/entries/Ordinal_Partitions.htmlA Formal Proof of The Chandy--Lamport Distributed Snapshot Algorithm
/entries/Chandy_Lamport.html
Tue, 21 Jul 2020 00:00:00 +0000/entries/Chandy_Lamport.htmlRelational Characterisations of Paths
/entries/Relational_Paths.html
Mon, 13 Jul 2020 00:00:00 +0000/entries/Relational_Paths.htmlA Formally Verified Checker of the Safe Distance Traffic Rules for Autonomous Vehicles
/entries/Safe_Distance.html
Mon, 01 Jun 2020 00:00:00 +0000/entries/Safe_Distance.htmlA verified algorithm for computing the Smith normal form of a matrix
/entries/Smith_Normal_Form.html
Sat, 23 May 2020 00:00:00 +0000/entries/Smith_Normal_Form.htmlThe Nash-Williams Partition Theorem
/entries/Nash_Williams.html
Sat, 16 May 2020 00:00:00 +0000/entries/Nash_Williams.htmlA Formalization of Knuth–Bendix Orders
/entries/Knuth_Bendix_Order.html
Wed, 13 May 2020 00:00:00 +0000/entries/Knuth_Bendix_Order.htmlIrrationality Criteria for Series by Erdős and Straus
/entries/Irrational_Series_Erdos_Straus.html
Tue, 12 May 2020 00:00:00 +0000/entries/Irrational_Series_Erdos_Straus.htmlRecursion Theorem in ZF
/entries/Recursion-Addition.html
Mon, 11 May 2020 00:00:00 +0000/entries/Recursion-Addition.htmlAn Efficient Normalisation Procedure for Linear Temporal Logic: Isabelle/HOL Formalisation
/entries/LTL_Normal_Form.html
Fri, 08 May 2020 00:00:00 +0000/entries/LTL_Normal_Form.htmlFormalization of Forcing in Isabelle/ZF
/entries/Forcing.html
Wed, 06 May 2020 00:00:00 +0000/entries/Forcing.htmlBanach-Steinhaus Theorem
/entries/Banach_Steinhaus.html
Sat, 02 May 2020 00:00:00 +0000/entries/Banach_Steinhaus.htmlAttack Trees in Isabelle for GDPR compliance of IoT healthcare systems
/entries/Attack_Trees.html
Mon, 27 Apr 2020 00:00:00 +0000/entries/Attack_Trees.htmlGaussian Integers
/entries/Gaussian_Integers.html
Fri, 24 Apr 2020 00:00:00 +0000/entries/Gaussian_Integers.htmlPower Sum Polynomials
/entries/Power_Sum_Polynomials.html
Fri, 24 Apr 2020 00:00:00 +0000/entries/Power_Sum_Polynomials.htmlThe Lambert W Function on the Reals
/entries/Lambert_W.html
Fri, 24 Apr 2020 00:00:00 +0000/entries/Lambert_W.htmlMatrices for ODEs
/entries/Matrices_for_ODEs.html
Sun, 19 Apr 2020 00:00:00 +0000/entries/Matrices_for_ODEs.htmlAuthenticated Data Structures As Functors
/entries/ADS_Functor.html
Thu, 16 Apr 2020 00:00:00 +0000/entries/ADS_Functor.htmlFormalization of an Algorithm for Greedily Computing Associative Aggregations on Sliding Windows
/entries/Sliding_Window_Algorithm.html
Fri, 10 Apr 2020 00:00:00 +0000/entries/Sliding_Window_Algorithm.htmlA Comprehensive Framework for Saturation Theorem Proving
/entries/Saturation_Framework.html
Thu, 09 Apr 2020 00:00:00 +0000/entries/Saturation_Framework.htmlFormalization of an Optimized Monitoring Algorithm for Metric First-Order Dynamic Logic with Aggregations
/entries/MFODL_Monitor_Optimized.html
Thu, 09 Apr 2020 00:00:00 +0000/entries/MFODL_Monitor_Optimized.htmlAutomated Stateful Protocol Verification
/entries/Automated_Stateful_Protocol_Verification.html
Wed, 08 Apr 2020 00:00:00 +0000/entries/Automated_Stateful_Protocol_Verification.htmlStateful Protocol Composition and Typing
/entries/Stateful_Protocol_Composition_and_Typing.html
Wed, 08 Apr 2020 00:00:00 +0000/entries/Stateful_Protocol_Composition_and_Typing.htmlLucas's Theorem
/entries/Lucas_Theorem.html
Tue, 07 Apr 2020 00:00:00 +0000/entries/Lucas_Theorem.htmlStrong Eventual Consistency of the Collaborative Editing Framework WOOT
/entries/WOOT_Strong_Eventual_Consistency.html
Wed, 25 Mar 2020 00:00:00 +0000/entries/WOOT_Strong_Eventual_Consistency.htmlFurstenberg's topology and his proof of the infinitude of primes
/entries/Furstenberg_Topology.html
Sun, 22 Mar 2020 00:00:00 +0000/entries/Furstenberg_Topology.htmlAn Under-Approximate Relational Logic
/entries/Relational-Incorrectness-Logic.html
Thu, 12 Mar 2020 00:00:00 +0000/entries/Relational-Incorrectness-Logic.htmlHello World
/entries/Hello_World.html
Sat, 07 Mar 2020 00:00:00 +0000/entries/Hello_World.htmlImplementing the Goodstein Function in λ-Calculus
/entries/Goodstein_Lambda.html
Fri, 21 Feb 2020 00:00:00 +0000/entries/Goodstein_Lambda.htmlA Generic Framework for Verified Compilers
/entries/VeriComp.html
Mon, 10 Feb 2020 00:00:00 +0000/entries/VeriComp.htmlArithmetic progressions and relative primes
/entries/Arith_Prog_Rel_Primes.html
Sat, 01 Feb 2020 00:00:00 +0000/entries/Arith_Prog_Rel_Primes.htmlA Hierarchy of Algebras for Boolean Subsets
/entries/Subset_Boolean_Algebras.html
Fri, 31 Jan 2020 00:00:00 +0000/entries/Subset_Boolean_Algebras.htmlMersenne primes and the Lucas–Lehmer test
/entries/Mersenne_Primes.html
Fri, 17 Jan 2020 00:00:00 +0000/entries/Mersenne_Primes.htmlVerified Approximation Algorithms
/entries/Approximation_Algorithms.html
Thu, 16 Jan 2020 00:00:00 +0000/entries/Approximation_Algorithms.htmlClosest Pair of Points Algorithms
/entries/Closest_Pair_Points.html
Mon, 13 Jan 2020 00:00:00 +0000/entries/Closest_Pair_Points.htmlSkip Lists
/entries/Skip_Lists.html
Thu, 09 Jan 2020 00:00:00 +0000/entries/Skip_Lists.htmlBicategories
/entries/Bicategory.html
Mon, 06 Jan 2020 00:00:00 +0000/entries/Bicategory.htmlThe Irrationality of ζ(3)
/entries/Zeta_3_Irrational.html
Fri, 27 Dec 2019 00:00:00 +0000/entries/Zeta_3_Irrational.htmlFormalizing a Seligman-Style Tableau System for Hybrid Logic
/entries/Hybrid_Logic.html
Fri, 20 Dec 2019 00:00:00 +0000/entries/Hybrid_Logic.htmlThe Poincaré-Bendixson Theorem
/entries/Poincare_Bendixson.html
Wed, 18 Dec 2019 00:00:00 +0000/entries/Poincare_Bendixson.htmlComplex Geometry
/entries/Complex_Geometry.html
Mon, 16 Dec 2019 00:00:00 +0000/entries/Complex_Geometry.htmlPoincaré Disc Model
/entries/Poincare_Disc.html
Mon, 16 Dec 2019 00:00:00 +0000/entries/Poincare_Disc.htmlGauss Sums and the Pólya–Vinogradov Inequality
/entries/Gauss_Sums.html
Tue, 10 Dec 2019 00:00:00 +0000/entries/Gauss_Sums.htmlAn Efficient Generalization of Counting Sort for Large, possibly Infinite Key Ranges
/entries/Generalized_Counting_Sort.html
Wed, 04 Dec 2019 00:00:00 +0000/entries/Generalized_Counting_Sort.htmlInterval Arithmetic on 32-bit Words
/entries/Interval_Arithmetic_Word32.html
Wed, 27 Nov 2019 00:00:00 +0000/entries/Interval_Arithmetic_Word32.htmlZermelo Fraenkel Set Theory in Higher-Order Logic
/entries/ZFC_in_HOL.html
Thu, 24 Oct 2019 00:00:00 +0000/entries/ZFC_in_HOL.htmlIsabelle/C
/entries/Isabelle_C.html
Tue, 22 Oct 2019 00:00:00 +0000/entries/Isabelle_C.htmlVerifyThis 2019 -- Polished Isabelle Solutions
/entries/VerifyThis2019.html
Wed, 16 Oct 2019 00:00:00 +0000/entries/VerifyThis2019.htmlAristotle's Assertoric Syllogistic
/entries/Aristotles_Assertoric_Syllogistic.html
Tue, 08 Oct 2019 00:00:00 +0000/entries/Aristotles_Assertoric_Syllogistic.htmlSigma Protocols and Commitment Schemes
/entries/Sigma_Commit_Crypto.html
Mon, 07 Oct 2019 00:00:00 +0000/entries/Sigma_Commit_Crypto.htmlClean - An Abstract Imperative Programming Language and its Theory
/entries/Clean.html
Fri, 04 Oct 2019 00:00:00 +0000/entries/Clean.htmlFormalization of Multiway-Join Algorithms
/entries/Generic_Join.html
Mon, 16 Sep 2019 00:00:00 +0000/entries/Generic_Join.htmlVerification Components for Hybrid Systems
/entries/Hybrid_Systems_VCs.html
Tue, 10 Sep 2019 00:00:00 +0000/entries/Hybrid_Systems_VCs.htmlFourier Series
/entries/Fourier.html
Fri, 06 Sep 2019 00:00:00 +0000/entries/Fourier.htmlA Case Study in Basic Algebra
/entries/Jacobson_Basic_Algebra.html
Fri, 30 Aug 2019 00:00:00 +0000/entries/Jacobson_Basic_Algebra.htmlFormalisation of an Adaptive State Counting Algorithm
/entries/Adaptive_State_Counting.html
Fri, 16 Aug 2019 00:00:00 +0000/entries/Adaptive_State_Counting.htmlLaplace Transform
/entries/Laplace_Transform.html
Wed, 14 Aug 2019 00:00:00 +0000/entries/Laplace_Transform.htmlCommunicating Concurrent Kleene Algebra for Distributed Systems Specification
/entries/C2KA_DistributedSystems.html
Tue, 06 Aug 2019 00:00:00 +0000/entries/C2KA_DistributedSystems.htmlLinear Programming
/entries/Linear_Programming.html
Tue, 06 Aug 2019 00:00:00 +0000/entries/Linear_Programming.htmlSelected Problems from the International Mathematical Olympiad 2019
/entries/IMO2019.html
Mon, 05 Aug 2019 00:00:00 +0000/entries/IMO2019.htmlStellar Quorum Systems
/entries/Stellar_Quorums.html
Thu, 01 Aug 2019 00:00:00 +0000/entries/Stellar_Quorums.htmlA Formal Development of a Polychronous Polytimed Coordination Language
/entries/TESL_Language.html
Tue, 30 Jul 2019 00:00:00 +0000/entries/TESL_Language.htmlOrder Extension and Szpilrajn's Extension Theorem
/entries/Szpilrajn.html
Sat, 27 Jul 2019 00:00:00 +0000/entries/Szpilrajn.htmlA Sequent Calculus for First-Order Logic
/entries/FOL_Seq_Calc1.html
Thu, 18 Jul 2019 00:00:00 +0000/entries/FOL_Seq_Calc1.htmlA Verified Code Generator from Isabelle/HOL to CakeML
/entries/CakeML_Codegen.html
Mon, 08 Jul 2019 00:00:00 +0000/entries/CakeML_Codegen.htmlFormalization of a Monitoring Algorithm for Metric First-Order Temporal Logic
/entries/MFOTL_Monitor.html
Thu, 04 Jul 2019 00:00:00 +0000/entries/MFOTL_Monitor.htmlComplete Non-Orders and Fixed Points
/entries/Complete_Non_Orders.html
Thu, 27 Jun 2019 00:00:00 +0000/entries/Complete_Non_Orders.htmlPriority Search Trees
/entries/Priority_Search_Trees.html
Tue, 25 Jun 2019 00:00:00 +0000/entries/Priority_Search_Trees.htmlPurely Functional, Simple, and Efficient Implementation of Prim and Dijkstra
/entries/Prim_Dijkstra_Simple.html
Tue, 25 Jun 2019 00:00:00 +0000/entries/Prim_Dijkstra_Simple.htmlLinear Inequalities
/entries/Linear_Inequalities.html
Fri, 21 Jun 2019 00:00:00 +0000/entries/Linear_Inequalities.htmlHilbert's Nullstellensatz
/entries/Nullstellensatz.html
Sun, 16 Jun 2019 00:00:00 +0000/entries/Nullstellensatz.htmlGröbner Bases, Macaulay Matrices and Dubé's Degree Bounds
/entries/Groebner_Macaulay.html
Sat, 15 Jun 2019 00:00:00 +0000/entries/Groebner_Macaulay.htmlBinary Heaps for IMP2
/entries/IMP2_Binary_Heap.html
Thu, 13 Jun 2019 00:00:00 +0000/entries/IMP2_Binary_Heap.htmlDifferential Game Logic
/entries/Differential_Game_Logic.html
Mon, 03 Jun 2019 00:00:00 +0000/entries/Differential_Game_Logic.htmlMultidimensional Binary Search Trees
/entries/KD_Tree.html
Thu, 30 May 2019 00:00:00 +0000/entries/KD_Tree.htmlFormalization of Generic Authenticated Data Structures
/entries/LambdaAuth.html
Tue, 14 May 2019 00:00:00 +0000/entries/LambdaAuth.htmlMulti-Party Computation
/entries/Multi_Party_Computation.html
Thu, 09 May 2019 00:00:00 +0000/entries/Multi_Party_Computation.htmlHOL-CSP Version 2.0
/entries/HOL-CSP.html
Fri, 26 Apr 2019 00:00:00 +0000/entries/HOL-CSP.htmlA Compositional and Unified Translation of LTL into ω-Automata
/entries/LTL_Master_Theorem.html
Tue, 16 Apr 2019 00:00:00 +0000/entries/LTL_Master_Theorem.htmlA General Theory of Syntax with Bindings
/entries/Binding_Syntax_Theory.html
Sat, 06 Apr 2019 00:00:00 +0000/entries/Binding_Syntax_Theory.htmlThe Transcendence of Certain Infinite Series
/entries/Transcendence_Series_Hancl_Rucki.html
Wed, 27 Mar 2019 00:00:00 +0000/entries/Transcendence_Series_Hancl_Rucki.htmlQuantum Hoare Logic
/entries/QHLProver.html
Sun, 24 Mar 2019 00:00:00 +0000/entries/QHLProver.htmlSafe OCL
/entries/Safe_OCL.html
Sat, 09 Mar 2019 00:00:00 +0000/entries/Safe_OCL.htmlElementary Facts About the Distribution of Primes
/entries/Prime_Distribution_Elementary.html
Thu, 21 Feb 2019 00:00:00 +0000/entries/Prime_Distribution_Elementary.htmlKruskal's Algorithm for Minimum Spanning Forest
/entries/Kruskal.html
Thu, 14 Feb 2019 00:00:00 +0000/entries/Kruskal.htmlProbabilistic Primality Testing
/entries/Probabilistic_Prime_Tests.html
Mon, 11 Feb 2019 00:00:00 +0000/entries/Probabilistic_Prime_Tests.htmlUniversal Turing Machine
/entries/Universal_Turing_Machine.html
Fri, 08 Feb 2019 00:00:00 +0000/entries/Universal_Turing_Machine.htmlIsabelle/UTP: Mechanised Theory Engineering for Unifying Theories of Programming
/entries/UTP.html
Fri, 01 Feb 2019 00:00:00 +0000/entries/UTP.htmlThe Inversions of a List
/entries/List_Inversions.html
Fri, 01 Feb 2019 00:00:00 +0000/entries/List_Inversions.htmlFarkas' Lemma and Motzkin's Transposition Theorem
/entries/Farkas.html
Thu, 17 Jan 2019 00:00:00 +0000/entries/Farkas.htmlAn Algebra for Higher-Order Terms
/entries/Higher_Order_Terms.html
Tue, 15 Jan 2019 00:00:00 +0000/entries/Higher_Order_Terms.htmlIMP2 – Simple Program Verification in Isabelle/HOL
/entries/IMP2.html
Tue, 15 Jan 2019 00:00:00 +0000/entries/IMP2.htmlA Reduction Theorem for Store Buffers
/entries/Store_Buffer_Reduction.html
Mon, 07 Jan 2019 00:00:00 +0000/entries/Store_Buffer_Reduction.htmlA Formal Model of the Document Object Model
/entries/Core_DOM.html
Wed, 26 Dec 2018 00:00:00 +0000/entries/Core_DOM.htmlFormalization of Concurrent Revisions
/entries/Concurrent_Revisions.html
Tue, 25 Dec 2018 00:00:00 +0000/entries/Concurrent_Revisions.htmlVerifying Imperative Programs using Auto2
/entries/Auto2_Imperative_HOL.html
Fri, 21 Dec 2018 00:00:00 +0000/entries/Auto2_Imperative_HOL.htmlConstructive Cryptography in HOL
/entries/Constructive_Cryptography.html
Mon, 17 Dec 2018 00:00:00 +0000/entries/Constructive_Cryptography.htmlProperties of Orderings and Lattices
/entries/Order_Lattice_Props.html
Tue, 11 Dec 2018 00:00:00 +0000/entries/Order_Lattice_Props.htmlQuantales
/entries/Quantales.html
Tue, 11 Dec 2018 00:00:00 +0000/entries/Quantales.htmlTransformer Semantics
/entries/Transformer_Semantics.html
Tue, 11 Dec 2018 00:00:00 +0000/entries/Transformer_Semantics.htmlA Verified Functional Implementation of Bachmair and Ganzinger's Ordered Resolution Prover
/entries/Functional_Ordered_Resolution_Prover.html
Fri, 23 Nov 2018 00:00:00 +0000/entries/Functional_Ordered_Resolution_Prover.htmlGraph Saturation
/entries/Graph_Saturation.html
Fri, 23 Nov 2018 00:00:00 +0000/entries/Graph_Saturation.htmlAuto2 Prover
/entries/Auto2_HOL.html
Tue, 20 Nov 2018 00:00:00 +0000/entries/Auto2_HOL.htmlMatroids
/entries/Matroids.html
Fri, 16 Nov 2018 00:00:00 +0000/entries/Matroids.htmlDeriving generic class instances for datatypes
/entries/Generic_Deriving.html
Tue, 06 Nov 2018 00:00:00 +0000/entries/Generic_Deriving.htmlFormalisation and Evaluation of Alan Gewirth's Proof for the Principle of Generic Consistency in Isabelle/HOL
/entries/GewirthPGCProof.html
Tue, 30 Oct 2018 00:00:00 +0000/entries/GewirthPGCProof.htmlEpistemic Logic: Completeness of Modal Logics
/entries/Epistemic_Logic.html
Mon, 29 Oct 2018 00:00:00 +0000/entries/Epistemic_Logic.htmlSmooth Manifolds
/entries/Smooth_Manifolds.html
Mon, 22 Oct 2018 00:00:00 +0000/entries/Smooth_Manifolds.htmlFormalization of the Embedding Path Order for Lambda-Free Higher-Order Terms
/entries/Lambda_Free_EPO.html
Fri, 19 Oct 2018 00:00:00 +0000/entries/Lambda_Free_EPO.htmlRandomised Binary Search Trees
/entries/Randomised_BSTs.html
Fri, 19 Oct 2018 00:00:00 +0000/entries/Randomised_BSTs.htmlUpper Bounding Diameters of State Spaces of Factored Transition Systems
/entries/Factored_Transition_System_Bounding.html
Fri, 12 Oct 2018 00:00:00 +0000/entries/Factored_Transition_System_Bounding.htmlThe Transcendence of π
/entries/Pi_Transcendental.html
Fri, 28 Sep 2018 00:00:00 +0000/entries/Pi_Transcendental.htmlSymmetric Polynomials
/entries/Symmetric_Polynomials.html
Tue, 25 Sep 2018 00:00:00 +0000/entries/Symmetric_Polynomials.htmlSignature-Based Gröbner Basis Algorithms
/entries/Signature_Groebner.html
Thu, 20 Sep 2018 00:00:00 +0000/entries/Signature_Groebner.htmlThe Prime Number Theorem
/entries/Prime_Number_Theorem.html
Wed, 19 Sep 2018 00:00:00 +0000/entries/Prime_Number_Theorem.htmlAggregation Algebras
/entries/Aggregation_Algebras.html
Sat, 15 Sep 2018 00:00:00 +0000/entries/Aggregation_Algebras.htmlOctonions
/entries/Octonions.html
Fri, 14 Sep 2018 00:00:00 +0000/entries/Octonions.htmlQuaternions
/entries/Quaternions.html
Wed, 05 Sep 2018 00:00:00 +0000/entries/Quaternions.htmlThe Budan-Fourier Theorem and Counting Real Roots with Multiplicity
/entries/Budan_Fourier.html
Sun, 02 Sep 2018 00:00:00 +0000/entries/Budan_Fourier.htmlAn Incremental Simplex Algorithm with Unsatisfiable Core Generation
/entries/Simplex.html
Fri, 24 Aug 2018 00:00:00 +0000/entries/Simplex.htmlMinsky Machines
/entries/Minsky_Machines.html
Tue, 14 Aug 2018 00:00:00 +0000/entries/Minsky_Machines.htmlPricing in discrete financial models
/entries/DiscretePricing.html
Mon, 16 Jul 2018 00:00:00 +0000/entries/DiscretePricing.htmlVon-Neumann-Morgenstern Utility Theorem
/entries/Neumann_Morgenstern_Utility.html
Wed, 04 Jul 2018 00:00:00 +0000/entries/Neumann_Morgenstern_Utility.htmlPell's Equation
/entries/Pell.html
Sat, 23 Jun 2018 00:00:00 +0000/entries/Pell.htmlProjective Geometry
/entries/Projective_Geometry.html
Thu, 14 Jun 2018 00:00:00 +0000/entries/Projective_Geometry.htmlThe Localization of a Commutative Ring
/entries/Localization_Ring.html
Thu, 14 Jun 2018 00:00:00 +0000/entries/Localization_Ring.htmlPartial Order Reduction
/entries/Partial_Order_Reduction.html
Tue, 05 Jun 2018 00:00:00 +0000/entries/Partial_Order_Reduction.htmlOptimal Binary Search Trees
/entries/Optimal_BST.html
Sun, 27 May 2018 00:00:00 +0000/entries/Optimal_BST.htmlHidden Markov Models
/entries/Hidden_Markov_Models.html
Fri, 25 May 2018 00:00:00 +0000/entries/Hidden_Markov_Models.htmlProbabilistic Timed Automata
/entries/Probabilistic_Timed_Automata.html
Thu, 24 May 2018 00:00:00 +0000/entries/Probabilistic_Timed_Automata.htmlAxiom Systems for Category Theory in Free Logic
/entries/AxiomaticCategoryTheory.html
Wed, 23 May 2018 00:00:00 +0000/entries/AxiomaticCategoryTheory.htmlIrrational Rapidly Convergent Series
/entries/Irrationality_J_Hancl.html
Wed, 23 May 2018 00:00:00 +0000/entries/Irrationality_J_Hancl.htmlMonadification, Memoization and Dynamic Programming
/entries/Monad_Memo_DP.html
Tue, 22 May 2018 00:00:00 +0000/entries/Monad_Memo_DP.htmlOpSets: Sequential Specifications for Replicated Datatypes
/entries/OpSets.html
Thu, 10 May 2018 00:00:00 +0000/entries/OpSets.htmlAn Isabelle/HOL Formalization of the Modular Assembly Kit for Security Properties
/entries/Modular_Assembly_Kit_Security.html
Mon, 07 May 2018 00:00:00 +0000/entries/Modular_Assembly_Kit_Security.htmlWebAssembly
/entries/WebAssembly.html
Sun, 29 Apr 2018 00:00:00 +0000/entries/WebAssembly.htmlVerifyThis 2018 - Polished Isabelle Solutions
/entries/VerifyThis2018.html
Fri, 27 Apr 2018 00:00:00 +0000/entries/VerifyThis2018.htmlBounded Natural Functors with Covariance and Contravariance
/entries/BNF_CC.html
Tue, 24 Apr 2018 00:00:00 +0000/entries/BNF_CC.htmlThe Incompatibility of Fishburn-Strategyproofness and Pareto-Efficiency
/entries/Fishburn_Impossibility.html
Thu, 22 Mar 2018 00:00:00 +0000/entries/Fishburn_Impossibility.htmlWeight-Balanced Trees
/entries/Weight_Balanced_Trees.html
Tue, 13 Mar 2018 00:00:00 +0000/entries/Weight_Balanced_Trees.htmlCakeML
/entries/CakeML.html
Mon, 12 Mar 2018 00:00:00 +0000/entries/CakeML.htmlA Theory of Architectural Design Patterns
/entries/Architectural_Design_Patterns.html
Thu, 01 Mar 2018 00:00:00 +0000/entries/Architectural_Design_Patterns.htmlHoare Logics for Time Bounds
/entries/Hoare_Time.html
Mon, 26 Feb 2018 00:00:00 +0000/entries/Hoare_Time.htmlA verified factorization algorithm for integer polynomials with polynomial complexity
/entries/LLL_Factorization.html
Tue, 06 Feb 2018 00:00:00 +0000/entries/LLL_Factorization.htmlFirst-Order Terms
/entries/First_Order_Terms.html
Tue, 06 Feb 2018 00:00:00 +0000/entries/First_Order_Terms.htmlThe Error Function
/entries/Error_Function.html
Tue, 06 Feb 2018 00:00:00 +0000/entries/Error_Function.htmlTreaps
/entries/Treaps.html
Tue, 06 Feb 2018 00:00:00 +0000/entries/Treaps.htmlA verified LLL algorithm
/entries/LLL_Basis_Reduction.html
Fri, 02 Feb 2018 00:00:00 +0000/entries/LLL_Basis_Reduction.htmlFormalization of Bachmair and Ganzinger's Ordered Resolution Prover
/entries/Ordered_Resolution_Prover.html
Thu, 18 Jan 2018 00:00:00 +0000/entries/Ordered_Resolution_Prover.htmlGromov Hyperbolicity
/entries/Gromov_Hyperbolicity.html
Tue, 16 Jan 2018 00:00:00 +0000/entries/Gromov_Hyperbolicity.htmlAn Isabelle/HOL formalisation of Green's Theorem
/entries/Green.html
Thu, 11 Jan 2018 00:00:00 +0000/entries/Green.htmlTaylor Models
/entries/Taylor_Models.html
Mon, 08 Jan 2018 00:00:00 +0000/entries/Taylor_Models.htmlThe Falling Factorial of a Sum
/entries/Falling_Factorial_Sum.html
Fri, 22 Dec 2017 00:00:00 +0000/entries/Falling_Factorial_Sum.htmlDirichlet L-Functions and Dirichlet's Theorem
/entries/Dirichlet_L.html
Thu, 21 Dec 2017 00:00:00 +0000/entries/Dirichlet_L.htmlThe Mason–Stothers Theorem
/entries/Mason_Stothers.html
Thu, 21 Dec 2017 00:00:00 +0000/entries/Mason_Stothers.htmlThe Median-of-Medians Selection Algorithm
/entries/Median_Of_Medians_Selection.html
Thu, 21 Dec 2017 00:00:00 +0000/entries/Median_Of_Medians_Selection.htmlOperations on Bounded Natural Functors
/entries/BNF_Operations.html
Tue, 19 Dec 2017 00:00:00 +0000/entries/BNF_Operations.htmlThe string search algorithm by Knuth, Morris and Pratt
/entries/Knuth_Morris_Pratt.html
Mon, 18 Dec 2017 00:00:00 +0000/entries/Knuth_Morris_Pratt.htmlStochastic Matrices and the Perron-Frobenius Theorem
/entries/Stochastic_Matrices.html
Wed, 22 Nov 2017 00:00:00 +0000/entries/Stochastic_Matrices.htmlThe IMAP CmRDT
/entries/IMAP-CRDT.html
Thu, 09 Nov 2017 00:00:00 +0000/entries/IMAP-CRDT.htmlHybrid Multi-Lane Spatial Logic
/entries/Hybrid_Multi_Lane_Spatial_Logic.html
Mon, 06 Nov 2017 00:00:00 +0000/entries/Hybrid_Multi_Lane_Spatial_Logic.htmlThe Kuratowski Closure-Complement Theorem
/entries/Kuratowski_Closure_Complement.html
Thu, 26 Oct 2017 00:00:00 +0000/entries/Kuratowski_Closure_Complement.htmlBüchi Complementation
/entries/Buchi_Complementation.html
Thu, 19 Oct 2017 00:00:00 +0000/entries/Buchi_Complementation.htmlTransition Systems and Automata
/entries/Transition_Systems_and_Automata.html
Thu, 19 Oct 2017 00:00:00 +0000/entries/Transition_Systems_and_Automata.htmlCount the Number of Complex Roots
/entries/Count_Complex_Roots.html
Tue, 17 Oct 2017 00:00:00 +0000/entries/Count_Complex_Roots.htmlEvaluate Winding Numbers through Cauchy Indices
/entries/Winding_Number_Eval.html
Tue, 17 Oct 2017 00:00:00 +0000/entries/Winding_Number_Eval.htmlHomogeneous Linear Diophantine Equations
/entries/Diophantine_Eqns_Lin_Hom.html
Sat, 14 Oct 2017 00:00:00 +0000/entries/Diophantine_Eqns_Lin_Hom.htmlDirichlet Series
/entries/Dirichlet_Series.html
Thu, 12 Oct 2017 00:00:00 +0000/entries/Dirichlet_Series.htmlLinear Recurrences
/entries/Linear_Recurrences.html
Thu, 12 Oct 2017 00:00:00 +0000/entries/Linear_Recurrences.htmlThe Hurwitz and Riemann ζ Functions
/entries/Zeta_Function.html
Thu, 12 Oct 2017 00:00:00 +0000/entries/Zeta_Function.htmlComputer-assisted Reconstruction and Assessment of E. J. Lowe's Modal Ontological Argument
/entries/Lowe_Ontological_Argument.html
Thu, 21 Sep 2017 00:00:00 +0000/entries/Lowe_Ontological_Argument.htmlRepresentation and Partial Automation of the Principia Logico-Metaphysica in Isabelle/HOL
/entries/PLM.html
Sun, 17 Sep 2017 00:00:00 +0000/entries/PLM.htmlAnselm's God in Isabelle/HOL
/entries/AnselmGod.html
Wed, 06 Sep 2017 00:00:00 +0000/entries/AnselmGod.htmlMicroeconomics and the First Welfare Theorem
/entries/First_Welfare_Theorem.html
Fri, 01 Sep 2017 00:00:00 +0000/entries/First_Welfare_Theorem.htmlOrbit-Stabiliser Theorem with Application to Rotational Symmetries
/entries/Orbit_Stabiliser.html
Sun, 20 Aug 2017 00:00:00 +0000/entries/Orbit_Stabiliser.htmlRoot-Balanced Tree
/entries/Root_Balanced_Tree.html
Sun, 20 Aug 2017 00:00:00 +0000/entries/Root_Balanced_Tree.htmlThe LambdaMu-calculus
/entries/LambdaMu.html
Wed, 16 Aug 2017 00:00:00 +0000/entries/LambdaMu.htmlStewart's Theorem and Apollonius' Theorem
/entries/Stewart_Apollonius.html
Mon, 31 Jul 2017 00:00:00 +0000/entries/Stewart_Apollonius.htmlDynamic Architectures
/entries/DynamicArchitectures.html
Fri, 28 Jul 2017 00:00:00 +0000/entries/DynamicArchitectures.htmlDeclarative Semantics for Functional Languages
/entries/Decl_Sem_Fun_PL.html
Fri, 21 Jul 2017 00:00:00 +0000/entries/Decl_Sem_Fun_PL.htmlHOLCF-Prelude
/entries/HOLCF-Prelude.html
Sat, 15 Jul 2017 00:00:00 +0000/entries/HOLCF-Prelude.htmlMinkowski's Theorem
/entries/Minkowskis_Theorem.html
Thu, 13 Jul 2017 00:00:00 +0000/entries/Minkowskis_Theorem.htmlVerified Metatheory and Type Inference for a Name-Carrying Simply-Typed Lambda Calculus
/entries/Name_Carrying_Type_Inference.html
Sun, 09 Jul 2017 00:00:00 +0000/entries/Name_Carrying_Type_Inference.htmlA framework for establishing Strong Eventual Consistency for Conflict-free Replicated Datatypes
/entries/CRDT.html
Fri, 07 Jul 2017 00:00:00 +0000/entries/CRDT.htmlStone-Kleene Relation Algebras
/entries/Stone_Kleene_Relation_Algebras.html
Thu, 06 Jul 2017 00:00:00 +0000/entries/Stone_Kleene_Relation_Algebras.htmlPropositional Proof Systems
/entries/Propositional_Proof_Systems.html
Wed, 21 Jun 2017 00:00:00 +0000/entries/Propositional_Proof_Systems.htmlPartial Semigroups and Convolution Algebras
/entries/PSemigroupsConvolution.html
Tue, 13 Jun 2017 00:00:00 +0000/entries/PSemigroupsConvolution.htmlBuffon's Needle Problem
/entries/Buffons_Needle.html
Tue, 06 Jun 2017 00:00:00 +0000/entries/Buffons_Needle.htmlFlow Networks and the Min-Cut-Max-Flow Theorem
/entries/Flow_Networks.html
Thu, 01 Jun 2017 00:00:00 +0000/entries/Flow_Networks.htmlFormalizing Push-Relabel Algorithms
/entries/Prpu_Maxflow.html
Thu, 01 Jun 2017 00:00:00 +0000/entries/Prpu_Maxflow.htmlOptics
/entries/Optics.html
Thu, 25 May 2017 00:00:00 +0000/entries/Optics.htmlDeveloping Security Protocols by Refinement
/entries/Security_Protocol_Refinement.html
Wed, 24 May 2017 00:00:00 +0000/entries/Security_Protocol_Refinement.htmlDictionary Construction
/entries/Dict_Construction.html
Wed, 24 May 2017 00:00:00 +0000/entries/Dict_Construction.htmlThe Floyd-Warshall Algorithm for Shortest Paths
/entries/Floyd_Warshall.html
Mon, 08 May 2017 00:00:00 +0000/entries/Floyd_Warshall.htmlCryptHOL
/entries/CryptHOL.html
Fri, 05 May 2017 00:00:00 +0000/entries/CryptHOL.htmlEffect polymorphism in higher-order logic
/entries/Monomorphic_Monad.html
Fri, 05 May 2017 00:00:00 +0000/entries/Monomorphic_Monad.htmlGame-based cryptography in HOL
/entries/Game_Based_Crypto.html
Fri, 05 May 2017 00:00:00 +0000/entries/Game_Based_Crypto.htmlMonad normalisation
/entries/Monad_Normalisation.html
Fri, 05 May 2017 00:00:00 +0000/entries/Monad_Normalisation.htmlProbabilistic while loop
/entries/Probabilistic_While.html
Fri, 05 May 2017 00:00:00 +0000/entries/Probabilistic_While.htmlMonoidal Categories
/entries/MonoidalCategory.html
Thu, 04 May 2017 00:00:00 +0000/entries/MonoidalCategory.htmlTypes, Tableaus and Gödel’s God in Isabelle/HOL
/entries/Types_Tableaus_and_Goedels_God.html
Mon, 01 May 2017 00:00:00 +0000/entries/Types_Tableaus_and_Goedels_God.htmlLocal Lexing
/entries/LocalLexing.html
Fri, 28 Apr 2017 00:00:00 +0000/entries/LocalLexing.htmlConstructor Functions
/entries/Constructor_Funs.html
Wed, 19 Apr 2017 00:00:00 +0000/entries/Constructor_Funs.htmlLazifying case constants
/entries/Lazy_Case.html
Tue, 18 Apr 2017 00:00:00 +0000/entries/Lazy_Case.htmlSubresultants
/entries/Subresultants.html
Thu, 06 Apr 2017 00:00:00 +0000/entries/Subresultants.htmlExpected Shape of Random Binary Search Trees
/entries/Random_BSTs.html
Tue, 04 Apr 2017 00:00:00 +0000/entries/Random_BSTs.htmlLower bound on comparison-based sorting algorithms
/entries/Comparison_Sort_Lower_Bound.html
Wed, 15 Mar 2017 00:00:00 +0000/entries/Comparison_Sort_Lower_Bound.htmlThe number of comparisons in QuickSort
/entries/Quick_Sort_Cost.html
Wed, 15 Mar 2017 00:00:00 +0000/entries/Quick_Sort_Cost.htmlThe Euler–MacLaurin Formula
/entries/Euler_MacLaurin.html
Fri, 10 Mar 2017 00:00:00 +0000/entries/Euler_MacLaurin.htmlThe Group Law for Elliptic Curves
/entries/Elliptic_Curves_Group_Law.html
Tue, 28 Feb 2017 00:00:00 +0000/entries/Elliptic_Curves_Group_Law.htmlMenger's Theorem
/entries/Menger.html
Sun, 26 Feb 2017 00:00:00 +0000/entries/Menger.htmlDifferential Dynamic Logic
/entries/Differential_Dynamic_Logic.html
Mon, 13 Feb 2017 00:00:00 +0000/entries/Differential_Dynamic_Logic.htmlAbstract Soundness
/entries/Abstract_Soundness.html
Fri, 10 Feb 2017 00:00:00 +0000/entries/Abstract_Soundness.htmlStone Relation Algebras
/entries/Stone_Relation_Algebras.html
Tue, 07 Feb 2017 00:00:00 +0000/entries/Stone_Relation_Algebras.htmlRefining Authenticated Key Agreement with Strong Adversaries
/entries/Key_Agreement_Strong_Adversaries.html
Tue, 31 Jan 2017 00:00:00 +0000/entries/Key_Agreement_Strong_Adversaries.htmlBernoulli Numbers
/entries/Bernoulli.html
Tue, 24 Jan 2017 00:00:00 +0000/entries/Bernoulli.htmlBertrand's postulate
/entries/Bertrands_Postulate.html
Tue, 17 Jan 2017 00:00:00 +0000/entries/Bertrands_Postulate.htmlMinimal Static Single Assignment Form
/entries/Minimal_SSA.html
Tue, 17 Jan 2017 00:00:00 +0000/entries/Minimal_SSA.htmlThe Transcendence of e
/entries/E_Transcendental.html
Thu, 12 Jan 2017 00:00:00 +0000/entries/E_Transcendental.htmlFormal Network Models and Their Application to Firewall Policies
/entries/UPF_Firewall.html
Sun, 08 Jan 2017 00:00:00 +0000/entries/UPF_Firewall.htmlVerification of a Diffie-Hellman Password-based Authentication Protocol by Extending the Inductive Method
/entries/Password_Authentication_Protocol.html
Tue, 03 Jan 2017 00:00:00 +0000/entries/Password_Authentication_Protocol.htmlFirst-Order Logic According to Harrison
/entries/FOL_Harrison.html
Sun, 01 Jan 2017 00:00:00 +0000/entries/FOL_Harrison.htmlConcurrent Refinement Algebra and Rely Quotients
/entries/Concurrent_Ref_Alg.html
Fri, 30 Dec 2016 00:00:00 +0000/entries/Concurrent_Ref_Alg.htmlThe Twelvefold Way
/entries/Twelvefold_Way.html
Thu, 29 Dec 2016 00:00:00 +0000/entries/Twelvefold_Way.htmlProof Strategy Language
/entries/Proof_Strategy_Language.html
Tue, 20 Dec 2016 00:00:00 +0000/entries/Proof_Strategy_Language.htmlParaconsistency
/entries/Paraconsistency.html
Wed, 07 Dec 2016 00:00:00 +0000/entries/Paraconsistency.htmlCOMPLX: A Verification Framework for Concurrent Imperative Programs
/entries/Complx.html
Tue, 29 Nov 2016 00:00:00 +0000/entries/Complx.htmlAbstract Interpretation of Annotated Commands
/entries/Abs_Int_ITP2012.html
Wed, 23 Nov 2016 00:00:00 +0000/entries/Abs_Int_ITP2012.htmlSeparata: Isabelle tactics for Separation Algebra
/entries/Separata.html
Wed, 16 Nov 2016 00:00:00 +0000/entries/Separata.htmlFormalization of Knuth–Bendix Orders for Lambda-Free Higher-Order Terms
/entries/Lambda_Free_KBOs.html
Sat, 12 Nov 2016 00:00:00 +0000/entries/Lambda_Free_KBOs.htmlFormalization of Nested Multisets, Hereditary Multisets, and Syntactic Ordinals
/entries/Nested_Multisets_Ordinals.html
Sat, 12 Nov 2016 00:00:00 +0000/entries/Nested_Multisets_Ordinals.htmlExpressiveness of Deep Learning
/entries/Deep_Learning.html
Thu, 10 Nov 2016 00:00:00 +0000/entries/Deep_Learning.htmlModal Logics for Nominal Transition Systems
/entries/Modal_Logics_for_NTS.html
Tue, 25 Oct 2016 00:00:00 +0000/entries/Modal_Logics_for_NTS.htmlStable Matching
/entries/Stable_Matching.html
Mon, 24 Oct 2016 00:00:00 +0000/entries/Stable_Matching.htmlLOFT — Verified Migration of Linux Firewalls to SDN
/entries/LOFT.html
Fri, 21 Oct 2016 00:00:00 +0000/entries/LOFT.htmlA formal model for the SPARCv8 ISA and a proof of non-interference for the LEON3 processor
/entries/SPARCv8.html
Wed, 19 Oct 2016 00:00:00 +0000/entries/SPARCv8.htmlSource Coding Theorem
/entries/Source_Coding_Theorem.html
Wed, 19 Oct 2016 00:00:00 +0000/entries/Source_Coding_Theorem.htmlThe Factorization Algorithm of Berlekamp and Zassenhaus
/entries/Berlekamp_Zassenhaus.html
Fri, 14 Oct 2016 00:00:00 +0000/entries/Berlekamp_Zassenhaus.htmlIntersecting Chords Theorem
/entries/Chord_Segments.html
Tue, 11 Oct 2016 00:00:00 +0000/entries/Chord_Segments.htmlLp spaces
/entries/Lp.html
Wed, 05 Oct 2016 00:00:00 +0000/entries/Lp.htmlFisher–Yates shuffle
/entries/Fisher_Yates.html
Fri, 30 Sep 2016 00:00:00 +0000/entries/Fisher_Yates.htmlAllen's Interval Calculus
/entries/Allen_Calculus.html
Thu, 29 Sep 2016 00:00:00 +0000/entries/Allen_Calculus.htmlFormalization of Recursive Path Orders for Lambda-Free Higher-Order Terms
/entries/Lambda_Free_RPOs.html
Fri, 23 Sep 2016 00:00:00 +0000/entries/Lambda_Free_RPOs.htmlIptables Semantics
/entries/Iptables_Semantics.html
Fri, 09 Sep 2016 00:00:00 +0000/entries/Iptables_Semantics.htmlA Variant of the Superposition Calculus
/entries/SuperCalc.html
Tue, 06 Sep 2016 00:00:00 +0000/entries/SuperCalc.htmlStone Algebras
/entries/Stone_Algebras.html
Tue, 06 Sep 2016 00:00:00 +0000/entries/Stone_Algebras.htmlStirling's formula
/entries/Stirling_Formula.html
Thu, 01 Sep 2016 00:00:00 +0000/entries/Stirling_Formula.htmlRouting
/entries/Routing.html
Wed, 31 Aug 2016 00:00:00 +0000/entries/Routing.htmlSimple Firewall
/entries/Simple_Firewall.html
Wed, 24 Aug 2016 00:00:00 +0000/entries/Simple_Firewall.htmlInfeasible Paths Elimination by Symbolic Execution Techniques: Proof of Correctness and Preservation of Paths
/entries/InfPathElimination.html
Thu, 18 Aug 2016 00:00:00 +0000/entries/InfPathElimination.htmlFormalizing the Edmonds-Karp Algorithm
/entries/EdmondsKarp_Maxflow.html
Fri, 12 Aug 2016 00:00:00 +0000/entries/EdmondsKarp_Maxflow.htmlThe Imperative Refinement Framework
/entries/Refine_Imperative_HOL.html
Mon, 08 Aug 2016 00:00:00 +0000/entries/Refine_Imperative_HOL.htmlPtolemy's Theorem
/entries/Ptolemys_Theorem.html
Sun, 07 Aug 2016 00:00:00 +0000/entries/Ptolemys_Theorem.htmlSurprise Paradox
/entries/Surprise_Paradox.html
Sun, 17 Jul 2016 00:00:00 +0000/entries/Surprise_Paradox.htmlPairing Heap
/entries/Pairing_Heap.html
Thu, 14 Jul 2016 00:00:00 +0000/entries/Pairing_Heap.htmlA Framework for Verifying Depth-First Search Algorithms
/entries/DFS_Framework.html
Tue, 05 Jul 2016 00:00:00 +0000/entries/DFS_Framework.htmlChamber Complexes, Coxeter Systems, and Buildings
/entries/Buildings.html
Fri, 01 Jul 2016 00:00:00 +0000/entries/Buildings.htmlThe Resolution Calculus for First-Order Logic
/entries/Resolution_FOL.html
Thu, 30 Jun 2016 00:00:00 +0000/entries/Resolution_FOL.htmlThe Z Property
/entries/Rewriting_Z.html
Thu, 30 Jun 2016 00:00:00 +0000/entries/Rewriting_Z.htmlCompositional Security-Preserving Refinement for Concurrent Imperative Programs
/entries/Dependent_SIFUM_Refinement.html
Tue, 28 Jun 2016 00:00:00 +0000/entries/Dependent_SIFUM_Refinement.htmlIP Addresses
/entries/IP_Addresses.html
Tue, 28 Jun 2016 00:00:00 +0000/entries/IP_Addresses.htmlCardinality of Multisets
/entries/Card_Multisets.html
Sun, 26 Jun 2016 00:00:00 +0000/entries/Card_Multisets.htmlCategory Theory with Adjunctions and Limits
/entries/Category3.html
Sun, 26 Jun 2016 00:00:00 +0000/entries/Category3.htmlA Dependent Security Type System for Concurrent Imperative Programs
/entries/Dependent_SIFUM_Type_Systems.html
Sat, 25 Jun 2016 00:00:00 +0000/entries/Dependent_SIFUM_Type_Systems.htmlCatalan Numbers
/entries/Catalan_Numbers.html
Tue, 21 Jun 2016 00:00:00 +0000/entries/Catalan_Numbers.htmlProgram Construction and Verification Components Based on Kleene Algebra
/entries/Algebraic_VCs.html
Sat, 18 Jun 2016 00:00:00 +0000/entries/Algebraic_VCs.htmlConservation of CSP Noninterference Security under Concurrent Composition
/entries/Noninterference_Concurrent_Composition.html
Mon, 13 Jun 2016 00:00:00 +0000/entries/Noninterference_Concurrent_Composition.htmlFinite Machine Word Library
/entries/Word_Lib.html
Thu, 09 Jun 2016 00:00:00 +0000/entries/Word_Lib.htmlTree Decomposition
/entries/Tree_Decomposition.html
Tue, 31 May 2016 00:00:00 +0000/entries/Tree_Decomposition.htmlCardinality of Equivalence Relations
/entries/Card_Equiv_Relations.html
Tue, 24 May 2016 00:00:00 +0000/entries/Card_Equiv_Relations.htmlPOSIX Lexing with Derivatives of Regular Expressions
/entries/Posix-Lexing.html
Tue, 24 May 2016 00:00:00 +0000/entries/Posix-Lexing.htmlPerron-Frobenius Theorem for Spectral Radius Analysis
/entries/Perron_Frobenius.html
Fri, 20 May 2016 00:00:00 +0000/entries/Perron_Frobenius.htmlThe meta theory of the Incredible Proof Machine
/entries/Incredible_Proof_Machine.html
Fri, 20 May 2016 00:00:00 +0000/entries/Incredible_Proof_Machine.htmlA Constructive Proof for FLP
/entries/FLP.html
Wed, 18 May 2016 00:00:00 +0000/entries/FLP.htmlA Formal Proof of the Max-Flow Min-Cut Theorem for Countable Networks
/entries/MFMC_Countable.html
Mon, 09 May 2016 00:00:00 +0000/entries/MFMC_Countable.htmlRandomised Social Choice Theory
/entries/Randomised_Social_Choice.html
Thu, 05 May 2016 00:00:00 +0000/entries/Randomised_Social_Choice.htmlSpivey's Generalized Recurrence for Bell Numbers
/entries/Bell_Numbers_Spivey.html
Wed, 04 May 2016 00:00:00 +0000/entries/Bell_Numbers_Spivey.htmlThe Incompatibility of SD-Efficiency and SD-Strategy-Proofness
/entries/SDS_Impossibility.html
Wed, 04 May 2016 00:00:00 +0000/entries/SDS_Impossibility.htmlGröbner Bases Theory
/entries/Groebner_Bases.html
Mon, 02 May 2016 00:00:00 +0000/entries/Groebner_Bases.htmlNo Faster-Than-Light Observers
/entries/No_FTL_observers.html
Thu, 28 Apr 2016 00:00:00 +0000/entries/No_FTL_observers.htmlA formalisation of the Cocke-Younger-Kasami algorithm
/entries/CYK.html
Wed, 27 Apr 2016 00:00:00 +0000/entries/CYK.htmlAlgorithms for Reduced Ordered Binary Decision Diagrams
/entries/ROBDD.html
Wed, 27 Apr 2016 00:00:00 +0000/entries/ROBDD.htmlConservation of CSP Noninterference Security under Sequential Composition
/entries/Noninterference_Sequential_Composition.html
Tue, 26 Apr 2016 00:00:00 +0000/entries/Noninterference_Sequential_Composition.htmlKleene Algebras with Domain
/entries/KAD.html
Tue, 12 Apr 2016 00:00:00 +0000/entries/KAD.htmlPropositional Resolution and Prime Implicates Generation
/entries/PropResPI.html
Fri, 11 Mar 2016 00:00:00 +0000/entries/PropResPI.htmlThe Cartan Fixed Point Theorems
/entries/Cartan_FP.html
Tue, 08 Mar 2016 00:00:00 +0000/entries/Cartan_FP.htmlTimed Automata
/entries/Timed_Automata.html
Tue, 08 Mar 2016 00:00:00 +0000/entries/Timed_Automata.htmlLinear Temporal Logic
/entries/LTL.html
Tue, 01 Mar 2016 00:00:00 +0000/entries/LTL.htmlAnalysis of List Update Algorithms
/entries/List_Update.html
Wed, 17 Feb 2016 00:00:00 +0000/entries/List_Update.htmlVerified Construction of Static Single Assignment Form
/entries/Formal_SSA.html
Fri, 05 Feb 2016 00:00:00 +0000/entries/Formal_SSA.htmlPolynomial Factorization
/entries/Polynomial_Factorization.html
Fri, 29 Jan 2016 00:00:00 +0000/entries/Polynomial_Factorization.htmlPolynomial Interpolation
/entries/Polynomial_Interpolation.html
Fri, 29 Jan 2016 00:00:00 +0000/entries/Polynomial_Interpolation.htmlKnot Theory
/entries/Knot_Theory.html
Wed, 20 Jan 2016 00:00:00 +0000/entries/Knot_Theory.htmlTensor Product of Matrices
/entries/Matrix_Tensor.html
Mon, 18 Jan 2016 00:00:00 +0000/entries/Matrix_Tensor.htmlCardinality of Number Partitions
/entries/Card_Number_Partitions.html
Thu, 14 Jan 2016 00:00:00 +0000/entries/Card_Number_Partitions.htmlBasic Geometric Properties of Triangles
/entries/Triangle.html
Mon, 28 Dec 2015 00:00:00 +0000/entries/Triangle.htmlDescartes' Rule of Signs
/entries/Descartes_Sign_Rule.html
Mon, 28 Dec 2015 00:00:00 +0000/entries/Descartes_Sign_Rule.htmlLiouville numbers
/entries/Liouville_Numbers.html
Mon, 28 Dec 2015 00:00:00 +0000/entries/Liouville_Numbers.htmlThe Divergence of the Prime Harmonic Series
/entries/Prime_Harmonic_Series.html
Mon, 28 Dec 2015 00:00:00 +0000/entries/Prime_Harmonic_Series.htmlAlgebraic Numbers in Isabelle/HOL
/entries/Algebraic_Numbers.html
Tue, 22 Dec 2015 00:00:00 +0000/entries/Algebraic_Numbers.htmlApplicative Lifting
/entries/Applicative_Lifting.html
Tue, 22 Dec 2015 00:00:00 +0000/entries/Applicative_Lifting.htmlThe Stern-Brocot Tree
/entries/Stern_Brocot.html
Tue, 22 Dec 2015 00:00:00 +0000/entries/Stern_Brocot.htmlCardinality of Set Partitions
/entries/Card_Partitions.html
Sat, 12 Dec 2015 00:00:00 +0000/entries/Card_Partitions.htmlLatin Square
/entries/Latin_Square.html
Wed, 02 Dec 2015 00:00:00 +0000/entries/Latin_Square.htmlErgodic Theory
/entries/Ergodic_Theory.html
Tue, 01 Dec 2015 00:00:00 +0000/entries/Ergodic_Theory.htmlEuler's Partition Theorem
/entries/Euler_Partition.html
Thu, 19 Nov 2015 00:00:00 +0000/entries/Euler_Partition.htmlThe Tortoise and Hare Algorithm
/entries/TortoiseHare.html
Wed, 18 Nov 2015 00:00:00 +0000/entries/TortoiseHare.htmlPlanarity Certificates
/entries/Planarity_Certificates.html
Wed, 11 Nov 2015 00:00:00 +0000/entries/Planarity_Certificates.htmlPositional Determinacy of Parity Games
/entries/Parity_Game.html
Mon, 02 Nov 2015 00:00:00 +0000/entries/Parity_Game.htmlA Meta-Model for the Isabelle API
/entries/Isabelle_Meta_Model.html
Wed, 16 Sep 2015 00:00:00 +0000/entries/Isabelle_Meta_Model.htmlConverting Linear Temporal Logic to Deterministic (Generalized) Rabin Automata
/entries/LTL_to_DRA.html
Fri, 04 Sep 2015 00:00:00 +0000/entries/LTL_to_DRA.htmlMatrices, Jordan Normal Forms, and Spectral Radius Theory
/entries/Jordan_Normal_Form.html
Fri, 21 Aug 2015 00:00:00 +0000/entries/Jordan_Normal_Form.htmlDecreasing Diagrams II
/entries/Decreasing-Diagrams-II.html
Thu, 20 Aug 2015 00:00:00 +0000/entries/Decreasing-Diagrams-II.htmlThe Inductive Unwinding Theorem for CSP Noninterference Security
/entries/Noninterference_Inductive_Unwinding.html
Tue, 18 Aug 2015 00:00:00 +0000/entries/Noninterference_Inductive_Unwinding.htmlRepresentations of Finite Groups
/entries/Rep_Fin_Groups.html
Wed, 12 Aug 2015 00:00:00 +0000/entries/Rep_Fin_Groups.htmlAnalysing and Comparing Encodability Criteria for Process Calculi
/entries/Encodability_Process_Calculi.html
Mon, 10 Aug 2015 00:00:00 +0000/entries/Encodability_Process_Calculi.htmlGenerating Cases from Labeled Subgoals
/entries/Case_Labeling.html
Tue, 21 Jul 2015 00:00:00 +0000/entries/Case_Labeling.htmlLandau Symbols
/entries/Landau_Symbols.html
Tue, 14 Jul 2015 00:00:00 +0000/entries/Landau_Symbols.htmlThe Akra-Bazzi theorem and the Master theorem
/entries/Akra_Bazzi.html
Tue, 14 Jul 2015 00:00:00 +0000/entries/Akra_Bazzi.htmlHermite Normal Form
/entries/Hermite.html
Tue, 07 Jul 2015 00:00:00 +0000/entries/Hermite.htmlDerangements Formula
/entries/Derangements.html
Sat, 27 Jun 2015 00:00:00 +0000/entries/Derangements.htmlBinary Multirelations
/entries/Multirelations.html
Thu, 11 Jun 2015 00:00:00 +0000/entries/Multirelations.htmlReasoning about Lists via List Interleaving
/entries/List_Interleaving.html
Thu, 11 Jun 2015 00:00:00 +0000/entries/List_Interleaving.htmlThe Generic Unwinding Theorem for CSP Noninterference Security
/entries/Noninterference_Generic_Unwinding.html
Thu, 11 Jun 2015 00:00:00 +0000/entries/Noninterference_Generic_Unwinding.htmlThe Ipurge Unwinding Theorem for CSP Noninterference Security
/entries/Noninterference_Ipurge_Unwinding.html
Thu, 11 Jun 2015 00:00:00 +0000/entries/Noninterference_Ipurge_Unwinding.htmlParameterized Dynamic Tables
/entries/Dynamic_Tables.html
Sun, 07 Jun 2015 00:00:00 +0000/entries/Dynamic_Tables.htmlDerivatives of Logical Formulas
/entries/Formula_Derivatives.html
Thu, 28 May 2015 00:00:00 +0000/entries/Formula_Derivatives.htmlA Zoo of Probabilistic Systems
/entries/Probabilistic_System_Zoo.html
Wed, 27 May 2015 00:00:00 +0000/entries/Probabilistic_System_Zoo.htmlVCG - Combinatorial Vickrey-Clarke-Groves Auctions
/entries/Vickrey_Clarke_Groves.html
Thu, 30 Apr 2015 00:00:00 +0000/entries/Vickrey_Clarke_Groves.htmlResiduated Lattices
/entries/Residuated_Lattices.html
Wed, 15 Apr 2015 00:00:00 +0000/entries/Residuated_Lattices.htmlConcurrent IMP
/entries/ConcurrentIMP.html
Mon, 13 Apr 2015 00:00:00 +0000/entries/ConcurrentIMP.htmlRelaxing Safely: Verified On-the-Fly Garbage Collection for x86-TSO
/entries/ConcurrentGC.html
Mon, 13 Apr 2015 00:00:00 +0000/entries/ConcurrentGC.htmlTrie
/entries/Trie.html
Mon, 30 Mar 2015 00:00:00 +0000/entries/Trie.htmlConsensus Refined
/entries/Consensus_Refined.html
Wed, 18 Mar 2015 00:00:00 +0000/entries/Consensus_Refined.htmlDeriving class instances for datatypes
/entries/Deriving.html
Wed, 11 Mar 2015 00:00:00 +0000/entries/Deriving.htmlThe Safety of Call Arity
/entries/Call_Arity.html
Fri, 20 Feb 2015 00:00:00 +0000/entries/Call_Arity.htmlEchelon Form
/entries/Echelon_Form.html
Thu, 12 Feb 2015 00:00:00 +0000/entries/Echelon_Form.htmlQR Decomposition
/entries/QR_Decomposition.html
Thu, 12 Feb 2015 00:00:00 +0000/entries/QR_Decomposition.htmlFinite Automata in Hereditarily Finite Set Theory
/entries/Finite_Automata_HF.html
Thu, 05 Feb 2015 00:00:00 +0000/entries/Finite_Automata_HF.htmlVerification of the UpDown Scheme
/entries/UpDown_Scheme.html
Wed, 28 Jan 2015 00:00:00 +0000/entries/UpDown_Scheme.htmlThe Unified Policy Framework (UPF)
/entries/UPF.html
Fri, 28 Nov 2014 00:00:00 +0000/entries/UPF.htmlLoop freedom of the (untimed) AODV routing protocol
/entries/AODV.html
Thu, 23 Oct 2014 00:00:00 +0000/entries/AODV.htmlLifting Definition Option
/entries/Lifting_Definition_Option.html
Mon, 13 Oct 2014 00:00:00 +0000/entries/Lifting_Definition_Option.htmlStream Fusion in HOL with Code Generation
/entries/Stream_Fusion_Code.html
Fri, 10 Oct 2014 00:00:00 +0000/entries/Stream_Fusion_Code.htmlA Verified Compiler for Probability Density Functions
/entries/Density_Compiler.html
Thu, 09 Oct 2014 00:00:00 +0000/entries/Density_Compiler.htmlFormalization of Refinement Calculus for Reactive Systems
/entries/RefinementReactive.html
Wed, 08 Oct 2014 00:00:00 +0000/entries/RefinementReactive.htmlCertification Monads
/entries/Certification_Monads.html
Fri, 03 Oct 2014 00:00:00 +0000/entries/Certification_Monads.htmlXML
/entries/XML.html
Fri, 03 Oct 2014 00:00:00 +0000/entries/XML.htmlImperative Insertion Sort
/entries/Imperative_Insertion_Sort.html
Thu, 25 Sep 2014 00:00:00 +0000/entries/Imperative_Insertion_Sort.htmlThe Sturm-Tarski Theorem
/entries/Sturm_Tarski.html
Fri, 19 Sep 2014 00:00:00 +0000/entries/Sturm_Tarski.htmlThe Cayley-Hamilton Theorem
/entries/Cayley_Hamilton.html
Mon, 15 Sep 2014 00:00:00 +0000/entries/Cayley_Hamilton.htmlThe Jordan-Hölder Theorem
/entries/Jordan_Hoelder.html
Tue, 09 Sep 2014 00:00:00 +0000/entries/Jordan_Hoelder.htmlPriority Queues Based on Braun Trees
/entries/Priority_Queue_Braun.html
Thu, 04 Sep 2014 00:00:00 +0000/entries/Priority_Queue_Braun.htmlGauss-Jordan Algorithm and Its Applications
/entries/Gauss_Jordan.html
Wed, 03 Sep 2014 00:00:00 +0000/entries/Gauss_Jordan.htmlReal-Valued Special Functions: Upper and Lower Bounds
/entries/Special_Function_Bounds.html
Fri, 29 Aug 2014 00:00:00 +0000/entries/Special_Function_Bounds.htmlVector Spaces
/entries/VectorSpace.html
Fri, 29 Aug 2014 00:00:00 +0000/entries/VectorSpace.htmlSkew Heap
/entries/Skew_Heap.html
Wed, 13 Aug 2014 00:00:00 +0000/entries/Skew_Heap.htmlSplay Tree
/entries/Splay_Tree.html
Tue, 12 Aug 2014 00:00:00 +0000/entries/Splay_Tree.htmlHaskell's Show Class in Isabelle/HOL
/entries/Show.html
Tue, 29 Jul 2014 00:00:00 +0000/entries/Show.htmlFormal Specification of a Generic Separation Kernel
/entries/CISC-Kernel.html
Fri, 18 Jul 2014 00:00:00 +0000/entries/CISC-Kernel.htmlpGCL for Isabelle
/entries/pGCL.html
Sun, 13 Jul 2014 00:00:00 +0000/entries/pGCL.htmlAmortized Complexity Verified
/entries/Amortized_Complexity.html
Mon, 07 Jul 2014 00:00:00 +0000/entries/Amortized_Complexity.htmlNetwork Security Policy Verification
/entries/Network_Security_Policy_Verification.html
Fri, 04 Jul 2014 00:00:00 +0000/entries/Network_Security_Policy_Verification.htmlPop-Refinement
/entries/Pop_Refinement.html
Thu, 03 Jul 2014 00:00:00 +0000/entries/Pop_Refinement.htmlDecision Procedures for MSO on Words Based on Derivatives of Regular Expressions
/entries/MSO_Regex_Equivalence.html
Thu, 12 Jun 2014 00:00:00 +0000/entries/MSO_Regex_Equivalence.htmlBoolean Expression Checkers
/entries/Boolean_Expression_Checkers.html
Sun, 08 Jun 2014 00:00:00 +0000/entries/Boolean_Expression_Checkers.htmlA Fully Verified Executable LTL Model Checker
/entries/CAVA_LTL_Modelchecker.html
Wed, 28 May 2014 00:00:00 +0000/entries/CAVA_LTL_Modelchecker.htmlConverting Linear-Time Temporal Logic to Generalized Büchi Automata
/entries/LTL_to_GBA.html
Wed, 28 May 2014 00:00:00 +0000/entries/LTL_to_GBA.htmlPromela Formalization
/entries/Promela.html
Wed, 28 May 2014 00:00:00 +0000/entries/Promela.htmlThe CAVA Automata Library
/entries/CAVA_Automata.html
Wed, 28 May 2014 00:00:00 +0000/entries/CAVA_Automata.htmlVerified Efficient Implementation of Gabow's Strongly Connected Components Algorithm
/entries/Gabow_SCC.html
Wed, 28 May 2014 00:00:00 +0000/entries/Gabow_SCC.htmlNoninterference Security in Communicating Sequential Processes
/entries/Noninterference_CSP.html
Fri, 23 May 2014 00:00:00 +0000/entries/Noninterference_CSP.htmlTransitive closure according to Roy-Floyd-Warshall
/entries/Roy_Floyd_Warshall.html
Fri, 23 May 2014 00:00:00 +0000/entries/Roy_Floyd_Warshall.htmlRegular Algebras
/entries/Regular_Algebras.html
Wed, 21 May 2014 00:00:00 +0000/entries/Regular_Algebras.htmlFormalisation and Analysis of Component Dependencies
/entries/ComponentDependencies.html
Mon, 28 Apr 2014 00:00:00 +0000/entries/ComponentDependencies.htmlA Formalization of Assumptions and Guarantees for Compositional Noninterference
/entries/SIFUM_Type_Systems.html
Wed, 23 Apr 2014 00:00:00 +0000/entries/SIFUM_Type_Systems.htmlA Formalization of Declassification with WHAT-and-WHERE-Security
/entries/WHATandWHERE_Security.html
Wed, 23 Apr 2014 00:00:00 +0000/entries/WHATandWHERE_Security.htmlA Formalization of Strong Security
/entries/Strong_Security.html
Wed, 23 Apr 2014 00:00:00 +0000/entries/Strong_Security.htmlBounded-Deducibility Security
/entries/Bounded_Deducibility_Security.html
Tue, 22 Apr 2014 00:00:00 +0000/entries/Bounded_Deducibility_Security.htmlA shallow embedding of HyperCTL*
/entries/HyperCTL.html
Wed, 16 Apr 2014 00:00:00 +0000/entries/HyperCTL.htmlAbstract Completeness
/entries/Abstract_Completeness.html
Wed, 16 Apr 2014 00:00:00 +0000/entries/Abstract_Completeness.htmlDiscrete Summation
/entries/Discrete_Summation.html
Sun, 13 Apr 2014 00:00:00 +0000/entries/Discrete_Summation.htmlSyntax and semantics of a GPU kernel programming language
/entries/GPU_Kernel_PL.html
Thu, 03 Apr 2014 00:00:00 +0000/entries/GPU_Kernel_PL.htmlProbabilistic Noninterference
/entries/Probabilistic_Noninterference.html
Tue, 11 Mar 2014 00:00:00 +0000/entries/Probabilistic_Noninterference.htmlMechanization of the Algebra for Wireless Networks (AWN)
/entries/AWN.html
Sat, 08 Mar 2014 00:00:00 +0000/entries/AWN.htmlMutually Recursive Partial Functions
/entries/Partial_Function_MR.html
Tue, 18 Feb 2014 00:00:00 +0000/entries/Partial_Function_MR.htmlProperties of Random Graphs -- Subgraph Containment
/entries/Random_Graph_Subgraph_Threshold.html
Thu, 13 Feb 2014 00:00:00 +0000/entries/Random_Graph_Subgraph_Threshold.htmlVerification of Selection and Heap Sort Using Locales
/entries/Selection_Heap_Sort.html
Tue, 11 Feb 2014 00:00:00 +0000/entries/Selection_Heap_Sort.htmlAffine Arithmetic
/entries/Affine_Arithmetic.html
Fri, 07 Feb 2014 00:00:00 +0000/entries/Affine_Arithmetic.htmlImplementing field extensions of the form Q[sqrt(b)]
/entries/Real_Impl.html
Thu, 06 Feb 2014 00:00:00 +0000/entries/Real_Impl.htmlUnified Decision Procedures for Regular Expression Equivalence
/entries/Regex_Equivalence.html
Thu, 30 Jan 2014 00:00:00 +0000/entries/Regex_Equivalence.htmlSecondary Sylow Theorems
/entries/Secondary_Sylow.html
Tue, 28 Jan 2014 00:00:00 +0000/entries/Secondary_Sylow.htmlRelation Algebra
/entries/Relation_Algebra.html
Sat, 25 Jan 2014 00:00:00 +0000/entries/Relation_Algebra.htmlKleene Algebra with Tests and Demonic Refinement Algebras
/entries/KAT_and_DRA.html
Thu, 23 Jan 2014 00:00:00 +0000/entries/KAT_and_DRA.htmlFeatherweight OCL: A Proposal for a Machine-Checked Formal Semantics for OCL 2.5
/entries/Featherweight_OCL.html
Thu, 16 Jan 2014 00:00:00 +0000/entries/Featherweight_OCL.htmlCompositional Properties of Crypto-Based Components
/entries/CryptoBasedCompositionalProperties.html
Sat, 11 Jan 2014 00:00:00 +0000/entries/CryptoBasedCompositionalProperties.htmlSturm's Theorem
/entries/Sturm_Sequences.html
Sat, 11 Jan 2014 00:00:00 +0000/entries/Sturm_Sequences.htmlA General Method for the Proof of Theorems on Tail-recursive Functions
/entries/Tail_Recursive_Functions.html
Sun, 01 Dec 2013 00:00:00 +0000/entries/Tail_Recursive_Functions.htmlGödel's Incompleteness Theorems
/entries/Incompleteness.html
Sun, 17 Nov 2013 00:00:00 +0000/entries/Incompleteness.htmlThe Hereditarily Finite Sets
/entries/HereditarilyFinite.html
Sun, 17 Nov 2013 00:00:00 +0000/entries/HereditarilyFinite.htmlA Codatatype of Formal Languages
/entries/Coinductive_Languages.html
Fri, 15 Nov 2013 00:00:00 +0000/entries/Coinductive_Languages.htmlStream Processing Components: Isabelle/HOL Formalisation and Case Studies
/entries/FocusStreamsCaseStudies.html
Thu, 14 Nov 2013 00:00:00 +0000/entries/FocusStreamsCaseStudies.htmlGödel's God in Isabelle/HOL
/entries/GoedelGod.html
Tue, 12 Nov 2013 00:00:00 +0000/entries/GoedelGod.htmlDecreasing Diagrams
/entries/Decreasing-Diagrams.html
Fri, 01 Nov 2013 00:00:00 +0000/entries/Decreasing-Diagrams.htmlAutomatic Data Refinement
/entries/Automatic_Refinement.html
Wed, 02 Oct 2013 00:00:00 +0000/entries/Automatic_Refinement.htmlNative Word
/entries/Native_Word.html
Tue, 17 Sep 2013 00:00:00 +0000/entries/Native_Word.htmlA Formal Model of IEEE Floating Point Arithmetic
/entries/IEEE_Floating_Point.html
Sat, 27 Jul 2013 00:00:00 +0000/entries/IEEE_Floating_Point.htmlLehmer's Theorem
/entries/Lehmer.html
Mon, 22 Jul 2013 00:00:00 +0000/entries/Lehmer.htmlPratt's Primality Certificates
/entries/Pratt_Certificate.html
Mon, 22 Jul 2013 00:00:00 +0000/entries/Pratt_Certificate.htmlThe Königsberg Bridge Problem and the Friendship Theorem
/entries/Koenigsberg_Friendship.html
Fri, 19 Jul 2013 00:00:00 +0000/entries/Koenigsberg_Friendship.htmlSound and Complete Sort Encodings for First-Order Logic
/entries/Sort_Encodings.html
Thu, 27 Jun 2013 00:00:00 +0000/entries/Sort_Encodings.htmlAn Axiomatic Characterization of the Single-Source Shortest Path Problem
/entries/ShortestPath.html
Wed, 22 May 2013 00:00:00 +0000/entries/ShortestPath.htmlGraph Theory
/entries/Graph_Theory.html
Sun, 28 Apr 2013 00:00:00 +0000/entries/Graph_Theory.htmlLight-weight Containers
/entries/Containers.html
Mon, 15 Apr 2013 00:00:00 +0000/entries/Containers.htmlNominal 2
/entries/Nominal2.html
Thu, 21 Feb 2013 00:00:00 +0000/entries/Nominal2.htmlThe Correctness of Launchbury's Natural Semantics for Lazy Evaluation
/entries/Launchbury.html
Thu, 31 Jan 2013 00:00:00 +0000/entries/Launchbury.htmlRibbon Proofs
/entries/Ribbon_Proofs.html
Sat, 19 Jan 2013 00:00:00 +0000/entries/Ribbon_Proofs.htmlRank-Nullity Theorem in Linear Algebra
/entries/Rank_Nullity_Theorem.html
Wed, 16 Jan 2013 00:00:00 +0000/entries/Rank_Nullity_Theorem.htmlKleene Algebra
/entries/Kleene_Algebra.html
Tue, 15 Jan 2013 00:00:00 +0000/entries/Kleene_Algebra.htmlComputing N-th Roots using the Babylonian Method
/entries/Sqrt_Babylonian.html
Thu, 03 Jan 2013 00:00:00 +0000/entries/Sqrt_Babylonian.htmlA Separation Logic Framework for Imperative HOL
/entries/Separation_Logic_Imperative_HOL.html
Wed, 14 Nov 2012 00:00:00 +0000/entries/Separation_Logic_Imperative_HOL.htmlOpen Induction
/entries/Open_Induction.html
Fri, 02 Nov 2012 00:00:00 +0000/entries/Open_Induction.htmlThe independence of Tarski's Euclidean axiom
/entries/Tarskis_Geometry.html
Tue, 30 Oct 2012 00:00:00 +0000/entries/Tarskis_Geometry.htmlBondy's Theorem
/entries/Bondy.html
Sat, 27 Oct 2012 00:00:00 +0000/entries/Bondy.htmlPossibilistic Noninterference
/entries/Possibilistic_Noninterference.html
Mon, 10 Sep 2012 00:00:00 +0000/entries/Possibilistic_Noninterference.htmlGenerating linear orders for datatypes
/entries/Datatype_Order_Generator.html
Tue, 07 Aug 2012 00:00:00 +0000/entries/Datatype_Order_Generator.htmlProving the Impossibility of Trisecting an Angle and Doubling the Cube
/entries/Impossible_Geometry.html
Sun, 05 Aug 2012 00:00:00 +0000/entries/Impossible_Geometry.htmlVerifying Fault-Tolerant Distributed Algorithms in the Heard-Of Model
/entries/Heard_Of.html
Fri, 27 Jul 2012 00:00:00 +0000/entries/Heard_Of.htmlLogical Relations for PCF
/entries/PCF.html
Sun, 01 Jul 2012 00:00:00 +0000/entries/PCF.htmlType Constructor Classes and Monad Transformers
/entries/Tycon.html
Tue, 26 Jun 2012 00:00:00 +0000/entries/Tycon.htmlCCS in nominal logic
/entries/CCS.html
Tue, 29 May 2012 00:00:00 +0000/entries/CCS.htmlPsi-calculi in Isabelle
/entries/Psi_Calculi.html
Tue, 29 May 2012 00:00:00 +0000/entries/Psi_Calculi.htmlThe pi-calculus in nominal logic
/entries/Pi_Calculus.html
Tue, 29 May 2012 00:00:00 +0000/entries/Pi_Calculus.htmlIsabelle/Circus
/entries/Circus.html
Sun, 27 May 2012 00:00:00 +0000/entries/Circus.htmlSeparation Algebra
/entries/Separation_Algebra.html
Fri, 11 May 2012 00:00:00 +0000/entries/Separation_Algebra.htmlStuttering Equivalence
/entries/Stuttering_Equivalence.html
Mon, 07 May 2012 00:00:00 +0000/entries/Stuttering_Equivalence.htmlInductive Study of Confidentiality
/entries/Inductive_Confidentiality.html
Wed, 02 May 2012 00:00:00 +0000/entries/Inductive_Confidentiality.htmlOrdinary Differential Equations
/entries/Ordinary_Differential_Equations.html
Thu, 26 Apr 2012 00:00:00 +0000/entries/Ordinary_Differential_Equations.htmlWell-Quasi-Orders
/entries/Well_Quasi_Orders.html
Fri, 13 Apr 2012 00:00:00 +0000/entries/Well_Quasi_Orders.htmlAbortable Linearizable Modules
/entries/Abortable_Linearizable_Modules.html
Thu, 01 Mar 2012 00:00:00 +0000/entries/Abortable_Linearizable_Modules.htmlExecutable Transitive Closures
/entries/Transitive-Closure-II.html
Wed, 29 Feb 2012 00:00:00 +0000/entries/Transitive-Closure-II.htmlA Probabilistic Proof of the Girth-Chromatic Number Theorem
/entries/Girth_Chromatic.html
Mon, 06 Feb 2012 00:00:00 +0000/entries/Girth_Chromatic.htmlDijkstra's Shortest Path Algorithm
/entries/Dijkstra_Shortest_Path.html
Mon, 30 Jan 2012 00:00:00 +0000/entries/Dijkstra_Shortest_Path.htmlRefinement for Monadic Programs
/entries/Refine_Monadic.html
Mon, 30 Jan 2012 00:00:00 +0000/entries/Refine_Monadic.htmlMarkov Models
/entries/Markov_Models.html
Tue, 03 Jan 2012 00:00:00 +0000/entries/Markov_Models.htmlA Definitional Encoding of TLA* in Isabelle/HOL
/entries/TLA.html
Sat, 19 Nov 2011 00:00:00 +0000/entries/TLA.htmlEfficient Mergesort
/entries/Efficient-Mergesort.html
Wed, 09 Nov 2011 00:00:00 +0000/entries/Efficient-Mergesort.htmlAlgebra of Monotonic Boolean Transformers
/entries/MonoBoolTranAlgebra.html
Thu, 22 Sep 2011 00:00:00 +0000/entries/MonoBoolTranAlgebra.htmlLattice Properties
/entries/LatticeProperties.html
Thu, 22 Sep 2011 00:00:00 +0000/entries/LatticeProperties.htmlPseudo Hoops
/entries/PseudoHoops.html
Thu, 22 Sep 2011 00:00:00 +0000/entries/PseudoHoops.htmlThe Myhill-Nerode Theorem Based on Regular Expressions
/entries/Myhill-Nerode.html
Fri, 26 Aug 2011 00:00:00 +0000/entries/Myhill-Nerode.htmlGauss-Jordan Elimination for Matrices Represented as Functions
/entries/Gauss-Jordan-Elim-Fun.html
Fri, 19 Aug 2011 00:00:00 +0000/entries/Gauss-Jordan-Elim-Fun.htmlMaximum Cardinality Matching
/entries/Max-Card-Matching.html
Thu, 21 Jul 2011 00:00:00 +0000/entries/Max-Card-Matching.htmlKnowledge-based programs
/entries/KBPs.html
Tue, 17 May 2011 00:00:00 +0000/entries/KBPs.htmlThe General Triangle Is Unique
/entries/General-Triangle.html
Fri, 01 Apr 2011 00:00:00 +0000/entries/General-Triangle.htmlExecutable Transitive Closures of Finite Relations
/entries/Transitive-Closure.html
Mon, 14 Mar 2011 00:00:00 +0000/entries/Transitive-Closure.htmlAutoFocus Stream Processing for Single-Clocking and Multi-Clocking Semantics
/entries/AutoFocus-Stream.html
Wed, 23 Feb 2011 00:00:00 +0000/entries/AutoFocus-Stream.htmlInfinite Lists
/entries/List-Infinite.html
Wed, 23 Feb 2011 00:00:00 +0000/entries/List-Infinite.htmlInterval Temporal Logic on Natural Numbers
/entries/Nat-Interval-Logic.html
Wed, 23 Feb 2011 00:00:00 +0000/entries/Nat-Interval-Logic.htmlLightweight Java
/entries/LightweightJava.html
Mon, 07 Feb 2011 00:00:00 +0000/entries/LightweightJava.htmlRIPEMD-160
/entries/RIPEMD-160-SPARK.html
Mon, 10 Jan 2011 00:00:00 +0000/entries/RIPEMD-160-SPARK.htmlLower Semicontinuous Functions
/entries/Lower_Semicontinuous.html
Sat, 08 Jan 2011 00:00:00 +0000/entries/Lower_Semicontinuous.htmlHall's Marriage Theorem
/entries/Marriage.html
Fri, 17 Dec 2010 00:00:00 +0000/entries/Marriage.htmlShivers' Control Flow Analysis
/entries/Shivers-CFA.html
Tue, 16 Nov 2010 00:00:00 +0000/entries/Shivers-CFA.htmlBinomial Heaps and Skew Binomial Heaps
/entries/Binomial-Heaps.html
Thu, 28 Oct 2010 00:00:00 +0000/entries/Binomial-Heaps.htmlFinger Trees
/entries/Finger-Trees.html
Thu, 28 Oct 2010 00:00:00 +0000/entries/Finger-Trees.htmlFunctional Binomial Queues
/entries/Binomial-Queues.html
Thu, 28 Oct 2010 00:00:00 +0000/entries/Binomial-Queues.htmlStrong Normalization of Moggis's Computational Metalanguage
/entries/Lam-ml-Normalization.html
Sun, 29 Aug 2010 00:00:00 +0000/entries/Lam-ml-Normalization.htmlExecutable Multivariate Polynomials
/entries/Polynomials.html
Tue, 10 Aug 2010 00:00:00 +0000/entries/Polynomials.htmlFormalizing Statecharts using Hierarchical Automata
/entries/Statecharts.html
Sun, 08 Aug 2010 00:00:00 +0000/entries/Statecharts.htmlFree Groups
/entries/Free-Groups.html
Thu, 24 Jun 2010 00:00:00 +0000/entries/Free-Groups.htmlCategory Theory
/entries/Category2.html
Sun, 20 Jun 2010 00:00:00 +0000/entries/Category2.htmlExecutable Matrix Operations on Matrices of Arbitrary Dimensions
/entries/Matrix.html
Thu, 17 Jun 2010 00:00:00 +0000/entries/Matrix.htmlAbstract Rewriting
/entries/Abstract-Rewriting.html
Mon, 14 Jun 2010 00:00:00 +0000/entries/Abstract-Rewriting.htmlSemantics and Data Refinement of Invariant Based Programs
/entries/DataRefinementIBP.html
Fri, 28 May 2010 00:00:00 +0000/entries/DataRefinementIBP.htmlVerification of the Deutsch-Schorr-Waite Graph Marking Algorithm using Data Refinement
/entries/GraphMarkingIBP.html
Fri, 28 May 2010 00:00:00 +0000/entries/GraphMarkingIBP.htmlA Complete Proof of the Robbins Conjecture
/entries/Robbins-Conjecture.html
Sat, 22 May 2010 00:00:00 +0000/entries/Robbins-Conjecture.htmlRegular Sets and Expressions
/entries/Regular-Sets.html
Wed, 12 May 2010 00:00:00 +0000/entries/Regular-Sets.htmlLocally Nameless Sigma Calculus
/entries/Locally-Nameless-Sigma.html
Fri, 30 Apr 2010 00:00:00 +0000/entries/Locally-Nameless-Sigma.htmlFree Boolean Algebra
/entries/Free-Boolean-Algebra.html
Mon, 29 Mar 2010 00:00:00 +0000/entries/Free-Boolean-Algebra.htmlInformation Flow Noninterference via Slicing
/entries/InformationFlowSlicing.html
Tue, 23 Mar 2010 00:00:00 +0000/entries/InformationFlowSlicing.htmlInter-Procedural Information Flow Noninterference via Slicing
/entries/InformationFlowSlicing_Inter.html
Tue, 23 Mar 2010 00:00:00 +0000/entries/InformationFlowSlicing_Inter.htmlList Index
/entries/List-Index.html
Sat, 20 Feb 2010 00:00:00 +0000/entries/List-Index.htmlCoinductive
/entries/Coinductive.html
Fri, 12 Feb 2010 00:00:00 +0000/entries/Coinductive.htmlA Fast SAT Solver for Isabelle in Standard ML
/entries/DPT-SAT-Solver.html
Wed, 09 Dec 2009 00:00:00 +0000/entries/DPT-SAT-Solver.htmlFormalizing the Logic-Automaton Connection
/entries/Presburger-Automata.html
Thu, 03 Dec 2009 00:00:00 +0000/entries/Presburger-Automata.htmlCollections Framework
/entries/Collections.html
Wed, 25 Nov 2009 00:00:00 +0000/entries/Collections.htmlTree Automata
/entries/Tree-Automata.html
Wed, 25 Nov 2009 00:00:00 +0000/entries/Tree-Automata.htmlPerfect Number Theorem
/entries/Perfect-Number-Thm.html
Sun, 22 Nov 2009 00:00:00 +0000/entries/Perfect-Number-Thm.htmlBacking up Slicing: Verifying the Interprocedural Two-Phase Horwitz-Reps-Binkley Slicer
/entries/HRB-Slicing.html
Fri, 13 Nov 2009 00:00:00 +0000/entries/HRB-Slicing.htmlThe Worker/Wrapper Transformation
/entries/WorkerWrapper.html
Fri, 30 Oct 2009 00:00:00 +0000/entries/WorkerWrapper.htmlOrdinals and Cardinals
/entries/Ordinals_and_Cardinals.html
Tue, 01 Sep 2009 00:00:00 +0000/entries/Ordinals_and_Cardinals.htmlInvertibility in Sequent Calculi
/entries/SequentInvertibility.html
Fri, 28 Aug 2009 00:00:00 +0000/entries/SequentInvertibility.htmlAn Example of a Cofinitary Group in Isabelle/HOL
/entries/CofGroups.html
Tue, 04 Aug 2009 00:00:00 +0000/entries/CofGroups.htmlCode Generation for Functions as Data
/entries/FinFun.html
Wed, 06 May 2009 00:00:00 +0000/entries/FinFun.htmlStream Fusion
/entries/Stream-Fusion.html
Wed, 29 Apr 2009 00:00:00 +0000/entries/Stream-Fusion.htmlA Bytecode Logic for JML and Types
/entries/BytecodeLogicJmlTypes.html
Fri, 12 Dec 2008 00:00:00 +0000/entries/BytecodeLogicJmlTypes.htmlSecure information flow and program logics
/entries/SIFPL.html
Mon, 10 Nov 2008 00:00:00 +0000/entries/SIFPL.htmlSome classical results in Social Choice Theory
/entries/SenSocialChoice.html
Sun, 09 Nov 2008 00:00:00 +0000/entries/SenSocialChoice.htmlFun With Tilings
/entries/FunWithTilings.html
Fri, 07 Nov 2008 00:00:00 +0000/entries/FunWithTilings.htmlThe Textbook Proof of Huffman's Algorithm
/entries/Huffman.html
Wed, 15 Oct 2008 00:00:00 +0000/entries/Huffman.htmlTowards Certified Slicing
/entries/Slicing.html
Tue, 16 Sep 2008 00:00:00 +0000/entries/Slicing.htmlA Correctness Proof for the Volpano/Smith Security Typing System
/entries/VolpanoSmith.html
Tue, 02 Sep 2008 00:00:00 +0000/entries/VolpanoSmith.htmlArrow and Gibbard-Satterthwaite
/entries/ArrowImpossibilityGS.html
Mon, 01 Sep 2008 00:00:00 +0000/entries/ArrowImpossibilityGS.htmlFun With Functions
/entries/FunWithFunctions.html
Tue, 26 Aug 2008 00:00:00 +0000/entries/FunWithFunctions.htmlFormal Verification of Modern SAT Solvers
/entries/SATSolverVerification.html
Wed, 23 Jul 2008 00:00:00 +0000/entries/SATSolverVerification.htmlRecursion Theory I
/entries/Recursion-Theory-I.html
Sat, 05 Apr 2008 00:00:00 +0000/entries/Recursion-Theory-I.htmlA Sequential Imperative Programming Language Syntax, Semantics, Hoare Logics and Verification Environment
/entries/Simpl.html
Fri, 29 Feb 2008 00:00:00 +0000/entries/Simpl.htmlBDD Normalisation
/entries/BDD.html
Fri, 29 Feb 2008 00:00:00 +0000/entries/BDD.htmlNormalization by Evaluation
/entries/NormByEval.html
Mon, 18 Feb 2008 00:00:00 +0000/entries/NormByEval.htmlQuantifier Elimination for Linear Arithmetic
/entries/LinearQuantifierElim.html
Fri, 11 Jan 2008 00:00:00 +0000/entries/LinearQuantifierElim.htmlFormalization of Conflict Analysis of Programs with Procedures, Thread Creation, and Monitors
/entries/Program-Conflict-Analysis.html
Fri, 14 Dec 2007 00:00:00 +0000/entries/Program-Conflict-Analysis.htmlJinja with Threads
/entries/JinjaThreads.html
Mon, 03 Dec 2007 00:00:00 +0000/entries/JinjaThreads.htmlMuch Ado About Two
/entries/MuchAdoAboutTwo.html
Tue, 06 Nov 2007 00:00:00 +0000/entries/MuchAdoAboutTwo.htmlFermat's Last Theorem for Exponents 3 and 4 and the Parametrisation of Pythagorean Triples
/entries/Fermat3_4.html
Sun, 12 Aug 2007 00:00:00 +0000/entries/Fermat3_4.htmlSums of Two and Four Squares
/entries/SumSquares.html
Sun, 12 Aug 2007 00:00:00 +0000/entries/SumSquares.htmlFundamental Properties of Valuation Theory and Hensel's Lemma
/entries/Valuation.html
Wed, 08 Aug 2007 00:00:00 +0000/entries/Valuation.htmlFirst-Order Logic According to Fitting
/entries/FOL-Fitting.html
Thu, 02 Aug 2007 00:00:00 +0000/entries/FOL-Fitting.htmlPOPLmark Challenge Via de Bruijn Indices
/entries/POPLmark-deBruijn.html
Thu, 02 Aug 2007 00:00:00 +0000/entries/POPLmark-deBruijn.htmlHotel Key Card System
/entries/HotelKeyCards.html
Sat, 09 Sep 2006 00:00:00 +0000/entries/HotelKeyCards.htmlAbstract Hoare Logics
/entries/Abstract-Hoare-Logics.html
Tue, 08 Aug 2006 00:00:00 +0000/entries/Abstract-Hoare-Logics.htmlFlyspeck I: Tame Graphs
/entries/Flyspeck-Tame.html
Mon, 22 May 2006 00:00:00 +0000/entries/Flyspeck-Tame.htmlCoreC++
/entries/CoreC++.html
Mon, 15 May 2006 00:00:00 +0000/entries/CoreC++.htmlA Theory of Featherweight Java in Isabelle/HOL
/entries/FeatherweightJava.html
Fri, 31 Mar 2006 00:00:00 +0000/entries/FeatherweightJava.htmlInstances of Schneider's generalized protocol of clock synchronization
/entries/ClockSynchInst.html
Wed, 15 Mar 2006 00:00:00 +0000/entries/ClockSynchInst.htmlCauchy's Mean Theorem and the Cauchy-Schwarz Inequality
/entries/Cauchy.html
Tue, 14 Mar 2006 00:00:00 +0000/entries/Cauchy.htmlCountable Ordinals
/entries/Ordinal.html
Fri, 11 Nov 2005 00:00:00 +0000/entries/Ordinal.htmlFast Fourier Transform
/entries/FFT.html
Wed, 12 Oct 2005 00:00:00 +0000/entries/FFT.htmlFormalization of a Generalized Protocol for Clock Synchronization
/entries/GenClock.html
Fri, 24 Jun 2005 00:00:00 +0000/entries/GenClock.htmlProving the Correctness of Disk Paxos
/entries/DiskPaxos.html
Wed, 22 Jun 2005 00:00:00 +0000/entries/DiskPaxos.htmlJive Data and Store Model
/entries/JiveDataStoreModel.html
Mon, 20 Jun 2005 00:00:00 +0000/entries/JiveDataStoreModel.htmlJinja is not Java
/entries/Jinja.html
Wed, 01 Jun 2005 00:00:00 +0000/entries/Jinja.htmlSHA1, RSA, PSS and more
/entries/RSAPSS.html
Mon, 02 May 2005 00:00:00 +0000/entries/RSAPSS.htmlCategory Theory to Yoneda's Lemma
/entries/Category.html
Thu, 21 Apr 2005 00:00:00 +0000/entries/Category.htmlFile Refinement
/entries/FileRefinement.html
Thu, 09 Dec 2004 00:00:00 +0000/entries/FileRefinement.htmlIntegration theory and random variables
/entries/Integration.html
Fri, 19 Nov 2004 00:00:00 +0000/entries/Integration.htmlA Mechanically Verified, Efficient, Sound and Complete Theorem Prover For First Order Logic
/entries/Verified-Prover.html
Tue, 28 Sep 2004 00:00:00 +0000/entries/Verified-Prover.htmlCompleteness theorem
/entries/Completeness.html
Mon, 20 Sep 2004 00:00:00 +0000/entries/Completeness.htmlRamsey's theorem, infinitary version
/entries/Ramsey-Infinite.html
Mon, 20 Sep 2004 00:00:00 +0000/entries/Ramsey-Infinite.htmlCompiling Exceptions Correctly
/entries/Compiling-Exceptions-Correctly.html
Fri, 09 Jul 2004 00:00:00 +0000/entries/Compiling-Exceptions-Correctly.htmlDepth First Search
/entries/Depth-First-Search.html
Thu, 24 Jun 2004 00:00:00 +0000/entries/Depth-First-Search.htmlGroups, Rings and Modules
/entries/Group-Ring-Module.html
Tue, 18 May 2004 00:00:00 +0000/entries/Group-Ring-Module.htmlLazy Lists II
/entries/Lazy-Lists-II.html
Mon, 26 Apr 2004 00:00:00 +0000/entries/Lazy-Lists-II.htmlTopology
/entries/Topology.html
Mon, 26 Apr 2004 00:00:00 +0000/entries/Topology.htmlBinary Search Trees
/entries/BinarySearchTree.html
Mon, 05 Apr 2004 00:00:00 +0000/entries/BinarySearchTree.htmlFunctional Automata
/entries/Functional-Automata.html
Tue, 30 Mar 2004 00:00:00 +0000/entries/Functional-Automata.htmlAVL Trees
/entries/AVL-Trees.html
Fri, 19 Mar 2004 00:00:00 +0000/entries/AVL-Trees.htmlMini ML
/entries/MiniML.html
Fri, 19 Mar 2004 00:00:00 +0000/entries/MiniML.htmlAbortable_Linearizable_Modules
/theories/abortable_linearizable_modules/
Mon, 01 Jan 0001 00:00:00 +0000/theories/abortable_linearizable_modules/About
/about/
Mon, 01 Jan 0001 00:00:00 +0000/about/The Archive of Formal Proofs is a collection of proof libraries, examples, and larger scientific developments, mechanically checked in the theorem prover Isabelle. It is organized in the way of a scientific journal. Submissions are refereed.
The archive repository is hosted on Heptapod to provide easy free access to archive entries. The entries are tested and maintained continuously against the current stable release of Isabelle. Older versions of archive entries will remain available.Abs_Int_ITP2012
/theories/abs_int_itp2012/
Mon, 01 Jan 0001 00:00:00 +0000/theories/abs_int_itp2012/Abstract-Hoare-Logics
/theories/abstract-hoare-logics/
Mon, 01 Jan 0001 00:00:00 +0000/theories/abstract-hoare-logics/Abstract-Rewriting
/theories/abstract-rewriting/
Mon, 01 Jan 0001 00:00:00 +0000/theories/abstract-rewriting/Abstract_Completeness
/theories/abstract_completeness/
Mon, 01 Jan 0001 00:00:00 +0000/theories/abstract_completeness/Abstract_Soundness
/theories/abstract_soundness/
Mon, 01 Jan 0001 00:00:00 +0000/theories/abstract_soundness/Ackermanns_not_PR
/theories/ackermanns_not_pr/
Mon, 01 Jan 0001 00:00:00 +0000/theories/ackermanns_not_pr/Actuarial_Mathematics
/theories/actuarial_mathematics/
Mon, 01 Jan 0001 00:00:00 +0000/theories/actuarial_mathematics/Adaptive_State_Counting
/theories/adaptive_state_counting/
Mon, 01 Jan 0001 00:00:00 +0000/theories/adaptive_state_counting/ADS_Functor
/theories/ads_functor/
Mon, 01 Jan 0001 00:00:00 +0000/theories/ads_functor/Affine_Arithmetic
/theories/affine_arithmetic/
Mon, 01 Jan 0001 00:00:00 +0000/theories/affine_arithmetic/Aggregation_Algebras
/theories/aggregation_algebras/
Mon, 01 Jan 0001 00:00:00 +0000/theories/aggregation_algebras/AI_Planning_Languages_Semantics
/theories/ai_planning_languages_semantics/
Mon, 01 Jan 0001 00:00:00 +0000/theories/ai_planning_languages_semantics/Akra_Bazzi
/theories/akra_bazzi/
Mon, 01 Jan 0001 00:00:00 +0000/theories/akra_bazzi/Algebraic_Numbers
/theories/algebraic_numbers/
Mon, 01 Jan 0001 00:00:00 +0000/theories/algebraic_numbers/Algebraic_VCs
/theories/algebraic_vcs/
Mon, 01 Jan 0001 00:00:00 +0000/theories/algebraic_vcs/Allen_Calculus
/theories/allen_calculus/
Mon, 01 Jan 0001 00:00:00 +0000/theories/allen_calculus/Amicable_Numbers
/theories/amicable_numbers/
Mon, 01 Jan 0001 00:00:00 +0000/theories/amicable_numbers/Amortized_Complexity
/theories/amortized_complexity/
Mon, 01 Jan 0001 00:00:00 +0000/theories/amortized_complexity/AnselmGod
/theories/anselmgod/
Mon, 01 Jan 0001 00:00:00 +0000/theories/anselmgod/AODV
/theories/aodv/
Mon, 01 Jan 0001 00:00:00 +0000/theories/aodv/Applicative_Lifting
/theories/applicative_lifting/
Mon, 01 Jan 0001 00:00:00 +0000/theories/applicative_lifting/Approximation_Algorithms
/theories/approximation_algorithms/
Mon, 01 Jan 0001 00:00:00 +0000/theories/approximation_algorithms/Architectural_Design_Patterns
/theories/architectural_design_patterns/
Mon, 01 Jan 0001 00:00:00 +0000/theories/architectural_design_patterns/Aristotles_Assertoric_Syllogistic
/theories/aristotles_assertoric_syllogistic/
Mon, 01 Jan 0001 00:00:00 +0000/theories/aristotles_assertoric_syllogistic/Arith_Prog_Rel_Primes
/theories/arith_prog_rel_primes/
Mon, 01 Jan 0001 00:00:00 +0000/theories/arith_prog_rel_primes/ArrowImpossibilityGS
/theories/arrowimpossibilitygs/
Mon, 01 Jan 0001 00:00:00 +0000/theories/arrowimpossibilitygs/Attack_Trees
/theories/attack_trees/
Mon, 01 Jan 0001 00:00:00 +0000/theories/attack_trees/Auto2_HOL
/theories/auto2_hol/
Mon, 01 Jan 0001 00:00:00 +0000/theories/auto2_hol/Auto2_Imperative_HOL
/theories/auto2_imperative_hol/
Mon, 01 Jan 0001 00:00:00 +0000/theories/auto2_imperative_hol/AutoFocus-Stream
/theories/autofocus-stream/
Mon, 01 Jan 0001 00:00:00 +0000/theories/autofocus-stream/Automated_Stateful_Protocol_Verification
/theories/automated_stateful_protocol_verification/
Mon, 01 Jan 0001 00:00:00 +0000/theories/automated_stateful_protocol_verification/Automatic_Refinement
/theories/automatic_refinement/
Mon, 01 Jan 0001 00:00:00 +0000/theories/automatic_refinement/AVL-Trees
/theories/avl-trees/
Mon, 01 Jan 0001 00:00:00 +0000/theories/avl-trees/AWN
/theories/awn/
Mon, 01 Jan 0001 00:00:00 +0000/theories/awn/AxiomaticCategoryTheory
/theories/axiomaticcategorytheory/
Mon, 01 Jan 0001 00:00:00 +0000/theories/axiomaticcategorytheory/Banach_Steinhaus
/theories/banach_steinhaus/
Mon, 01 Jan 0001 00:00:00 +0000/theories/banach_steinhaus/BD_Security_Compositional
/theories/bd_security_compositional/
Mon, 01 Jan 0001 00:00:00 +0000/theories/bd_security_compositional/BDD
/theories/bdd/
Mon, 01 Jan 0001 00:00:00 +0000/theories/bdd/Belief_Revision
/theories/belief_revision/
Mon, 01 Jan 0001 00:00:00 +0000/theories/belief_revision/Bell_Numbers_Spivey
/theories/bell_numbers_spivey/
Mon, 01 Jan 0001 00:00:00 +0000/theories/bell_numbers_spivey/BenOr_Kozen_Reif
/theories/benor_kozen_reif/
Mon, 01 Jan 0001 00:00:00 +0000/theories/benor_kozen_reif/Berlekamp_Zassenhaus
/theories/berlekamp_zassenhaus/
Mon, 01 Jan 0001 00:00:00 +0000/theories/berlekamp_zassenhaus/Bernoulli
/theories/bernoulli/
Mon, 01 Jan 0001 00:00:00 +0000/theories/bernoulli/Bertrands_Postulate
/theories/bertrands_postulate/
Mon, 01 Jan 0001 00:00:00 +0000/theories/bertrands_postulate/Bicategory
/theories/bicategory/
Mon, 01 Jan 0001 00:00:00 +0000/theories/bicategory/BinarySearchTree
/theories/binarysearchtree/
Mon, 01 Jan 0001 00:00:00 +0000/theories/binarysearchtree/Binding_Syntax_Theory
/theories/binding_syntax_theory/
Mon, 01 Jan 0001 00:00:00 +0000/theories/binding_syntax_theory/Binomial-Heaps
/theories/binomial-heaps/
Mon, 01 Jan 0001 00:00:00 +0000/theories/binomial-heaps/Binomial-Queues
/theories/binomial-queues/
Mon, 01 Jan 0001 00:00:00 +0000/theories/binomial-queues/BirdKMP
/theories/birdkmp/
Mon, 01 Jan 0001 00:00:00 +0000/theories/birdkmp/Blue_Eyes
/theories/blue_eyes/
Mon, 01 Jan 0001 00:00:00 +0000/theories/blue_eyes/BNF_CC
/theories/bnf_cc/
Mon, 01 Jan 0001 00:00:00 +0000/theories/bnf_cc/BNF_Operations
/theories/bnf_operations/
Mon, 01 Jan 0001 00:00:00 +0000/theories/bnf_operations/Bondy
/theories/bondy/
Mon, 01 Jan 0001 00:00:00 +0000/theories/bondy/Boolean_Expression_Checkers
/theories/boolean_expression_checkers/
Mon, 01 Jan 0001 00:00:00 +0000/theories/boolean_expression_checkers/Bounded_Deducibility_Security
/theories/bounded_deducibility_security/
Mon, 01 Jan 0001 00:00:00 +0000/theories/bounded_deducibility_security/BTree
/theories/btree/
Mon, 01 Jan 0001 00:00:00 +0000/theories/btree/Buchi_Complementation
/theories/buchi_complementation/
Mon, 01 Jan 0001 00:00:00 +0000/theories/buchi_complementation/Budan_Fourier
/theories/budan_fourier/
Mon, 01 Jan 0001 00:00:00 +0000/theories/budan_fourier/Buffons_Needle
/theories/buffons_needle/
Mon, 01 Jan 0001 00:00:00 +0000/theories/buffons_needle/Buildings
/theories/buildings/
Mon, 01 Jan 0001 00:00:00 +0000/theories/buildings/BytecodeLogicJmlTypes
/theories/bytecodelogicjmltypes/
Mon, 01 Jan 0001 00:00:00 +0000/theories/bytecodelogicjmltypes/C2KA_DistributedSystems
/theories/c2ka_distributedsystems/
Mon, 01 Jan 0001 00:00:00 +0000/theories/c2ka_distributedsystems/CakeML
/theories/cakeml/
Mon, 01 Jan 0001 00:00:00 +0000/theories/cakeml/CakeML_Codegen
/theories/cakeml_codegen/
Mon, 01 Jan 0001 00:00:00 +0000/theories/cakeml_codegen/Call_Arity
/theories/call_arity/
Mon, 01 Jan 0001 00:00:00 +0000/theories/call_arity/Card_Equiv_Relations
/theories/card_equiv_relations/
Mon, 01 Jan 0001 00:00:00 +0000/theories/card_equiv_relations/Card_Multisets
/theories/card_multisets/
Mon, 01 Jan 0001 00:00:00 +0000/theories/card_multisets/Card_Number_Partitions
/theories/card_number_partitions/
Mon, 01 Jan 0001 00:00:00 +0000/theories/card_number_partitions/Card_Partitions
/theories/card_partitions/
Mon, 01 Jan 0001 00:00:00 +0000/theories/card_partitions/Cartan_FP
/theories/cartan_fp/
Mon, 01 Jan 0001 00:00:00 +0000/theories/cartan_fp/Case_Labeling
/theories/case_labeling/
Mon, 01 Jan 0001 00:00:00 +0000/theories/case_labeling/Catalan_Numbers
/theories/catalan_numbers/
Mon, 01 Jan 0001 00:00:00 +0000/theories/catalan_numbers/Category
/theories/category/
Mon, 01 Jan 0001 00:00:00 +0000/theories/category/Category2
/theories/category2/
Mon, 01 Jan 0001 00:00:00 +0000/theories/category2/Category3
/theories/category3/
Mon, 01 Jan 0001 00:00:00 +0000/theories/category3/Cauchy
/theories/cauchy/
Mon, 01 Jan 0001 00:00:00 +0000/theories/cauchy/CAVA_Automata
/theories/cava_automata/
Mon, 01 Jan 0001 00:00:00 +0000/theories/cava_automata/CAVA_Base
/theories/cava_base/
Mon, 01 Jan 0001 00:00:00 +0000/theories/cava_base/CAVA_LTL_Modelchecker
/theories/cava_ltl_modelchecker/
Mon, 01 Jan 0001 00:00:00 +0000/theories/cava_ltl_modelchecker/CAVA_Setup
/theories/cava_setup/
Mon, 01 Jan 0001 00:00:00 +0000/theories/cava_setup/Cayley_Hamilton
/theories/cayley_hamilton/
Mon, 01 Jan 0001 00:00:00 +0000/theories/cayley_hamilton/CCS
/theories/ccs/
Mon, 01 Jan 0001 00:00:00 +0000/theories/ccs/Certification_Monads
/theories/certification_monads/
Mon, 01 Jan 0001 00:00:00 +0000/theories/certification_monads/Chandy_Lamport
/theories/chandy_lamport/
Mon, 01 Jan 0001 00:00:00 +0000/theories/chandy_lamport/Chord_Segments
/theories/chord_segments/
Mon, 01 Jan 0001 00:00:00 +0000/theories/chord_segments/Circus
/theories/circus/
Mon, 01 Jan 0001 00:00:00 +0000/theories/circus/CISC-Kernel
/theories/cisc-kernel/
Mon, 01 Jan 0001 00:00:00 +0000/theories/cisc-kernel/Clean
/theories/clean/
Mon, 01 Jan 0001 00:00:00 +0000/theories/clean/Clique_and_Monotone_Circuits
/theories/clique_and_monotone_circuits/
Mon, 01 Jan 0001 00:00:00 +0000/theories/clique_and_monotone_circuits/ClockSynchInst
/theories/clocksynchinst/
Mon, 01 Jan 0001 00:00:00 +0000/theories/clocksynchinst/Closest_Pair_Points
/theories/closest_pair_points/
Mon, 01 Jan 0001 00:00:00 +0000/theories/closest_pair_points/CoCon
/theories/cocon/
Mon, 01 Jan 0001 00:00:00 +0000/theories/cocon/CofGroups
/theories/cofgroups/
Mon, 01 Jan 0001 00:00:00 +0000/theories/cofgroups/Coinductive
/theories/coinductive/
Mon, 01 Jan 0001 00:00:00 +0000/theories/coinductive/Coinductive_Languages
/theories/coinductive_languages/
Mon, 01 Jan 0001 00:00:00 +0000/theories/coinductive_languages/Collections
/theories/collections/
Mon, 01 Jan 0001 00:00:00 +0000/theories/collections/Collections_Examples
/theories/collections_examples/
Mon, 01 Jan 0001 00:00:00 +0000/theories/collections_examples/Combinable_Wands
/theories/combinable_wands/
Mon, 01 Jan 0001 00:00:00 +0000/theories/combinable_wands/Combinatorics_Words
/theories/combinatorics_words/
Mon, 01 Jan 0001 00:00:00 +0000/theories/combinatorics_words/Combinatorics_Words_Graph_Lemma
/theories/combinatorics_words_graph_lemma/
Mon, 01 Jan 0001 00:00:00 +0000/theories/combinatorics_words_graph_lemma/Combinatorics_Words_Lyndon
/theories/combinatorics_words_lyndon/
Mon, 01 Jan 0001 00:00:00 +0000/theories/combinatorics_words_lyndon/Comparison_Sort_Lower_Bound
/theories/comparison_sort_lower_bound/
Mon, 01 Jan 0001 00:00:00 +0000/theories/comparison_sort_lower_bound/Compiling-Exceptions-Correctly
/theories/compiling-exceptions-correctly/
Mon, 01 Jan 0001 00:00:00 +0000/theories/compiling-exceptions-correctly/Complete_Non_Orders
/theories/complete_non_orders/
Mon, 01 Jan 0001 00:00:00 +0000/theories/complete_non_orders/Completeness
/theories/completeness/
Mon, 01 Jan 0001 00:00:00 +0000/theories/completeness/Complex_Bounded_Operators
/theories/complex_bounded_operators/
Mon, 01 Jan 0001 00:00:00 +0000/theories/complex_bounded_operators/Complex_Geometry
/theories/complex_geometry/
Mon, 01 Jan 0001 00:00:00 +0000/theories/complex_geometry/Complx
/theories/complx/
Mon, 01 Jan 0001 00:00:00 +0000/theories/complx/ComponentDependencies
/theories/componentdependencies/
Mon, 01 Jan 0001 00:00:00 +0000/theories/componentdependencies/Concurrent_Ref_Alg
/theories/concurrent_ref_alg/
Mon, 01 Jan 0001 00:00:00 +0000/theories/concurrent_ref_alg/Concurrent_Revisions
/theories/concurrent_revisions/
Mon, 01 Jan 0001 00:00:00 +0000/theories/concurrent_revisions/ConcurrentGC
/theories/concurrentgc/
Mon, 01 Jan 0001 00:00:00 +0000/theories/concurrentgc/ConcurrentIMP
/theories/concurrentimp/
Mon, 01 Jan 0001 00:00:00 +0000/theories/concurrentimp/Conditional_Simplification
/theories/conditional_simplification/
Mon, 01 Jan 0001 00:00:00 +0000/theories/conditional_simplification/Conditional_Transfer_Rule
/theories/conditional_transfer_rule/
Mon, 01 Jan 0001 00:00:00 +0000/theories/conditional_transfer_rule/Consensus_Refined
/theories/consensus_refined/
Mon, 01 Jan 0001 00:00:00 +0000/theories/consensus_refined/Constructive_Cryptography
/theories/constructive_cryptography/
Mon, 01 Jan 0001 00:00:00 +0000/theories/constructive_cryptography/Constructive_Cryptography_CM
/theories/constructive_cryptography_cm/
Mon, 01 Jan 0001 00:00:00 +0000/theories/constructive_cryptography_cm/Constructor_Funs
/theories/constructor_funs/
Mon, 01 Jan 0001 00:00:00 +0000/theories/constructor_funs/Containers
/theories/containers/
Mon, 01 Jan 0001 00:00:00 +0000/theories/containers/Containers-Benchmarks
/theories/containers-benchmarks/
Mon, 01 Jan 0001 00:00:00 +0000/theories/containers-benchmarks/Core_DOM
/theories/core_dom/
Mon, 01 Jan 0001 00:00:00 +0000/theories/core_dom/Core_SC_DOM
/theories/core_sc_dom/
Mon, 01 Jan 0001 00:00:00 +0000/theories/core_sc_dom/CoreC++
/theories/corec++/
Mon, 01 Jan 0001 00:00:00 +0000/theories/corec++/Correctness_Algebras
/theories/correctness_algebras/
Mon, 01 Jan 0001 00:00:00 +0000/theories/correctness_algebras/CoSMed
/theories/cosmed/
Mon, 01 Jan 0001 00:00:00 +0000/theories/cosmed/CoSMeDis
/theories/cosmedis/
Mon, 01 Jan 0001 00:00:00 +0000/theories/cosmedis/Cotangent_PFD_Formula
/theories/cotangent_pfd_formula/
Mon, 01 Jan 0001 00:00:00 +0000/theories/cotangent_pfd_formula/Count_Complex_Roots
/theories/count_complex_roots/
Mon, 01 Jan 0001 00:00:00 +0000/theories/count_complex_roots/CRDT
/theories/crdt/
Mon, 01 Jan 0001 00:00:00 +0000/theories/crdt/CryptHOL
/theories/crypthol/
Mon, 01 Jan 0001 00:00:00 +0000/theories/crypthol/CryptoBasedCompositionalProperties
/theories/cryptobasedcompositionalproperties/
Mon, 01 Jan 0001 00:00:00 +0000/theories/cryptobasedcompositionalproperties/CSP_RefTK
/theories/csp_reftk/
Mon, 01 Jan 0001 00:00:00 +0000/theories/csp_reftk/Cubic_Quartic_Equations
/theories/cubic_quartic_equations/
Mon, 01 Jan 0001 00:00:00 +0000/theories/cubic_quartic_equations/CYK
/theories/cyk/
Mon, 01 Jan 0001 00:00:00 +0000/theories/cyk/CZH_Elementary_Categories
/theories/czh_elementary_categories/
Mon, 01 Jan 0001 00:00:00 +0000/theories/czh_elementary_categories/CZH_Foundations
/theories/czh_foundations/
Mon, 01 Jan 0001 00:00:00 +0000/theories/czh_foundations/CZH_Universal_Constructions
/theories/czh_universal_constructions/
Mon, 01 Jan 0001 00:00:00 +0000/theories/czh_universal_constructions/DataRefinementIBP
/theories/datarefinementibp/
Mon, 01 Jan 0001 00:00:00 +0000/theories/datarefinementibp/Datatype_Order_Generator
/theories/datatype_order_generator/
Mon, 01 Jan 0001 00:00:00 +0000/theories/datatype_order_generator/Decl_Sem_Fun_PL
/theories/decl_sem_fun_pl/
Mon, 01 Jan 0001 00:00:00 +0000/theories/decl_sem_fun_pl/Decreasing-Diagrams
/theories/decreasing-diagrams/
Mon, 01 Jan 0001 00:00:00 +0000/theories/decreasing-diagrams/Decreasing-Diagrams-II
/theories/decreasing-diagrams-ii/
Mon, 01 Jan 0001 00:00:00 +0000/theories/decreasing-diagrams-ii/Dedekind_Real
/theories/dedekind_real/
Mon, 01 Jan 0001 00:00:00 +0000/theories/dedekind_real/Deep_Learning
/theories/deep_learning/
Mon, 01 Jan 0001 00:00:00 +0000/theories/deep_learning/Delta_System_Lemma
/theories/delta_system_lemma/
Mon, 01 Jan 0001 00:00:00 +0000/theories/delta_system_lemma/Density_Compiler
/theories/density_compiler/
Mon, 01 Jan 0001 00:00:00 +0000/theories/density_compiler/Dependent_SIFUM_Refinement
/theories/dependent_sifum_refinement/
Mon, 01 Jan 0001 00:00:00 +0000/theories/dependent_sifum_refinement/Dependent_SIFUM_Type_Systems
/theories/dependent_sifum_type_systems/
Mon, 01 Jan 0001 00:00:00 +0000/theories/dependent_sifum_type_systems/Depth-First-Search
/theories/depth-first-search/
Mon, 01 Jan 0001 00:00:00 +0000/theories/depth-first-search/Derangements
/theories/derangements/
Mon, 01 Jan 0001 00:00:00 +0000/theories/derangements/Deriving
/theories/deriving/
Mon, 01 Jan 0001 00:00:00 +0000/theories/deriving/Descartes_Sign_Rule
/theories/descartes_sign_rule/
Mon, 01 Jan 0001 00:00:00 +0000/theories/descartes_sign_rule/Design_Theory
/theories/design_theory/
Mon, 01 Jan 0001 00:00:00 +0000/theories/design_theory/DFS_Framework
/theories/dfs_framework/
Mon, 01 Jan 0001 00:00:00 +0000/theories/dfs_framework/Dict_Construction
/theories/dict_construction/
Mon, 01 Jan 0001 00:00:00 +0000/theories/dict_construction/Differential_Dynamic_Logic
/theories/differential_dynamic_logic/
Mon, 01 Jan 0001 00:00:00 +0000/theories/differential_dynamic_logic/Differential_Game_Logic
/theories/differential_game_logic/
Mon, 01 Jan 0001 00:00:00 +0000/theories/differential_game_logic/Digit_Expansions
/theories/digit_expansions/
Mon, 01 Jan 0001 00:00:00 +0000/theories/digit_expansions/Dijkstra_Shortest_Path
/theories/dijkstra_shortest_path/
Mon, 01 Jan 0001 00:00:00 +0000/theories/dijkstra_shortest_path/Diophantine_Eqns_Lin_Hom
/theories/diophantine_eqns_lin_hom/
Mon, 01 Jan 0001 00:00:00 +0000/theories/diophantine_eqns_lin_hom/Dirichlet_L
/theories/dirichlet_l/
Mon, 01 Jan 0001 00:00:00 +0000/theories/dirichlet_l/Dirichlet_Series
/theories/dirichlet_series/
Mon, 01 Jan 0001 00:00:00 +0000/theories/dirichlet_series/Discrete_Summation
/theories/discrete_summation/
Mon, 01 Jan 0001 00:00:00 +0000/theories/discrete_summation/DiscretePricing
/theories/discretepricing/
Mon, 01 Jan 0001 00:00:00 +0000/theories/discretepricing/DiskPaxos
/theories/diskpaxos/
Mon, 01 Jan 0001 00:00:00 +0000/theories/diskpaxos/DOM_Components
/theories/dom_components/
Mon, 01 Jan 0001 00:00:00 +0000/theories/dom_components/Dominance_CHK
/theories/dominance_chk/
Mon, 01 Jan 0001 00:00:00 +0000/theories/dominance_chk/Download the Archive
/download/
Mon, 01 Jan 0001 00:00:00 +0000/download/Current stable version (for most recent Isabelle release): Download all sessions: afp-current.tar.gz (~70 MB)
Older stable versions: Please use the sourceforge download system to access older versions of the archive.
Mercurial access: At Heptapod (development version of the Archive, for the development version of Isabelle)
Metadata download The metadata of all entries is available as an array of JSON objects: metadata.json (~1 MB)
How to refer to AFP entries: You can refer to AFP entries by using the AFP as an Isabelle component.DPRM_Theorem
/theories/dprm_theorem/
Mon, 01 Jan 0001 00:00:00 +0000/theories/dprm_theorem/DPT-SAT-Solver
/theories/dpt-sat-solver/
Mon, 01 Jan 0001 00:00:00 +0000/theories/dpt-sat-solver/Dynamic_Tables
/theories/dynamic_tables/
Mon, 01 Jan 0001 00:00:00 +0000/theories/dynamic_tables/DynamicArchitectures
/theories/dynamicarchitectures/
Mon, 01 Jan 0001 00:00:00 +0000/theories/dynamicarchitectures/E_Transcendental
/theories/e_transcendental/
Mon, 01 Jan 0001 00:00:00 +0000/theories/e_transcendental/Echelon_Form
/theories/echelon_form/
Mon, 01 Jan 0001 00:00:00 +0000/theories/echelon_form/EdmondsKarp_Maxflow
/theories/edmondskarp_maxflow/
Mon, 01 Jan 0001 00:00:00 +0000/theories/edmondskarp_maxflow/Efficient-Mergesort
/theories/efficient-mergesort/
Mon, 01 Jan 0001 00:00:00 +0000/theories/efficient-mergesort/Elliptic_Curves_Group_Law
/theories/elliptic_curves_group_law/
Mon, 01 Jan 0001 00:00:00 +0000/theories/elliptic_curves_group_law/Encodability_Process_Calculi
/theories/encodability_process_calculi/
Mon, 01 Jan 0001 00:00:00 +0000/theories/encodability_process_calculi/Entry Submission
/submission/
Mon, 01 Jan 0001 00:00:00 +0000/submission/Submission Guidelines The submission must follow the following Isabelle style rules. For additional guidelines on Isabelle proofs, also see the this guide (feel free to follow all of these; only the below are mandatory). Technical details about the submission process and the format of the submission are explained on the submission site.
No use of the commands sorry or back. Instantiations must not use Isabelle-generated names such as xa — use Isar, the subgoal command or rename_tac to avoid such names.Epistemic_Logic
/theories/epistemic_logic/
Mon, 01 Jan 0001 00:00:00 +0000/theories/epistemic_logic/Equivalence_Relation_Enumeration
/theories/equivalence_relation_enumeration/
Mon, 01 Jan 0001 00:00:00 +0000/theories/equivalence_relation_enumeration/Ergodic_Theory
/theories/ergodic_theory/
Mon, 01 Jan 0001 00:00:00 +0000/theories/ergodic_theory/Error_Function
/theories/error_function/
Mon, 01 Jan 0001 00:00:00 +0000/theories/error_function/Euler_MacLaurin
/theories/euler_maclaurin/
Mon, 01 Jan 0001 00:00:00 +0000/theories/euler_maclaurin/Euler_Partition
/theories/euler_partition/
Mon, 01 Jan 0001 00:00:00 +0000/theories/euler_partition/Eval_FO
/theories/eval_fo/
Mon, 01 Jan 0001 00:00:00 +0000/theories/eval_fo/Extended_Finite_State_Machine_Inference
/theories/extended_finite_state_machine_inference/
Mon, 01 Jan 0001 00:00:00 +0000/theories/extended_finite_state_machine_inference/Extended_Finite_State_Machines
/theories/extended_finite_state_machines/
Mon, 01 Jan 0001 00:00:00 +0000/theories/extended_finite_state_machines/Factor_Algebraic_Polynomial
/theories/factor_algebraic_polynomial/
Mon, 01 Jan 0001 00:00:00 +0000/theories/factor_algebraic_polynomial/Factored_Transition_System_Bounding
/theories/factored_transition_system_bounding/
Mon, 01 Jan 0001 00:00:00 +0000/theories/factored_transition_system_bounding/Falling_Factorial_Sum
/theories/falling_factorial_sum/
Mon, 01 Jan 0001 00:00:00 +0000/theories/falling_factorial_sum/Farkas
/theories/farkas/
Mon, 01 Jan 0001 00:00:00 +0000/theories/farkas/Featherweight_OCL
/theories/featherweight_ocl/
Mon, 01 Jan 0001 00:00:00 +0000/theories/featherweight_ocl/FeatherweightJava
/theories/featherweightjava/
Mon, 01 Jan 0001 00:00:00 +0000/theories/featherweightjava/Fermat3_4
/theories/fermat3_4/
Mon, 01 Jan 0001 00:00:00 +0000/theories/fermat3_4/FFT
/theories/fft/
Mon, 01 Jan 0001 00:00:00 +0000/theories/fft/FileRefinement
/theories/filerefinement/
Mon, 01 Jan 0001 00:00:00 +0000/theories/filerefinement/FinFun
/theories/finfun/
Mon, 01 Jan 0001 00:00:00 +0000/theories/finfun/Finger-Trees
/theories/finger-trees/
Mon, 01 Jan 0001 00:00:00 +0000/theories/finger-trees/Finite-Map-Extras
/theories/finite-map-extras/
Mon, 01 Jan 0001 00:00:00 +0000/theories/finite-map-extras/Finite_Automata_HF
/theories/finite_automata_hf/
Mon, 01 Jan 0001 00:00:00 +0000/theories/finite_automata_hf/Finite_Fields
/theories/finite_fields/
Mon, 01 Jan 0001 00:00:00 +0000/theories/finite_fields/Finitely_Generated_Abelian_Groups
/theories/finitely_generated_abelian_groups/
Mon, 01 Jan 0001 00:00:00 +0000/theories/finitely_generated_abelian_groups/First_Order_Terms
/theories/first_order_terms/
Mon, 01 Jan 0001 00:00:00 +0000/theories/first_order_terms/First_Welfare_Theorem
/theories/first_welfare_theorem/
Mon, 01 Jan 0001 00:00:00 +0000/theories/first_welfare_theorem/Fishburn_Impossibility
/theories/fishburn_impossibility/
Mon, 01 Jan 0001 00:00:00 +0000/theories/fishburn_impossibility/Fisher_Yates
/theories/fisher_yates/
Mon, 01 Jan 0001 00:00:00 +0000/theories/fisher_yates/Fishers_Inequality
/theories/fishers_inequality/
Mon, 01 Jan 0001 00:00:00 +0000/theories/fishers_inequality/Flow_Networks
/theories/flow_networks/
Mon, 01 Jan 0001 00:00:00 +0000/theories/flow_networks/Floyd_Warshall
/theories/floyd_warshall/
Mon, 01 Jan 0001 00:00:00 +0000/theories/floyd_warshall/FLP
/theories/flp/
Mon, 01 Jan 0001 00:00:00 +0000/theories/flp/Flyspeck-Tame
/theories/flyspeck-tame/
Mon, 01 Jan 0001 00:00:00 +0000/theories/flyspeck-tame/Flyspeck-Tame-Computation
/theories/flyspeck-tame-computation/
Mon, 01 Jan 0001 00:00:00 +0000/theories/flyspeck-tame-computation/FO_Theory_Rewriting
/theories/fo_theory_rewriting/
Mon, 01 Jan 0001 00:00:00 +0000/theories/fo_theory_rewriting/FocusStreamsCaseStudies
/theories/focusstreamscasestudies/
Mon, 01 Jan 0001 00:00:00 +0000/theories/focusstreamscasestudies/FOL-Fitting
/theories/fol-fitting/
Mon, 01 Jan 0001 00:00:00 +0000/theories/fol-fitting/FOL_Axiomatic
/theories/fol_axiomatic/
Mon, 01 Jan 0001 00:00:00 +0000/theories/fol_axiomatic/FOL_Harrison
/theories/fol_harrison/
Mon, 01 Jan 0001 00:00:00 +0000/theories/fol_harrison/FOL_Seq_Calc1
/theories/fol_seq_calc1/
Mon, 01 Jan 0001 00:00:00 +0000/theories/fol_seq_calc1/FOL_Seq_Calc2
/theories/fol_seq_calc2/
Mon, 01 Jan 0001 00:00:00 +0000/theories/fol_seq_calc2/FOL_Seq_Calc3
/theories/fol_seq_calc3/
Mon, 01 Jan 0001 00:00:00 +0000/theories/fol_seq_calc3/Forcing
/theories/forcing/
Mon, 01 Jan 0001 00:00:00 +0000/theories/forcing/Formal_Puiseux_Series
/theories/formal_puiseux_series/
Mon, 01 Jan 0001 00:00:00 +0000/theories/formal_puiseux_series/Formal_SSA
/theories/formal_ssa/
Mon, 01 Jan 0001 00:00:00 +0000/theories/formal_ssa/Formula_Derivatives
/theories/formula_derivatives/
Mon, 01 Jan 0001 00:00:00 +0000/theories/formula_derivatives/Formula_Derivatives-Examples
/theories/formula_derivatives-examples/
Mon, 01 Jan 0001 00:00:00 +0000/theories/formula_derivatives-examples/Foundation_of_geometry
/theories/foundation_of_geometry/
Mon, 01 Jan 0001 00:00:00 +0000/theories/foundation_of_geometry/Fourier
/theories/fourier/
Mon, 01 Jan 0001 00:00:00 +0000/theories/fourier/Free-Boolean-Algebra
/theories/free-boolean-algebra/
Mon, 01 Jan 0001 00:00:00 +0000/theories/free-boolean-algebra/Free-Groups
/theories/free-groups/
Mon, 01 Jan 0001 00:00:00 +0000/theories/free-groups/Frequency_Moments
/theories/frequency_moments/
Mon, 01 Jan 0001 00:00:00 +0000/theories/frequency_moments/Fresh_Identifiers
/theories/fresh_identifiers/
Mon, 01 Jan 0001 00:00:00 +0000/theories/fresh_identifiers/Functional-Automata
/theories/functional-automata/
Mon, 01 Jan 0001 00:00:00 +0000/theories/functional-automata/Functional_Ordered_Resolution_Prover
/theories/functional_ordered_resolution_prover/
Mon, 01 Jan 0001 00:00:00 +0000/theories/functional_ordered_resolution_prover/FunWithFunctions
/theories/funwithfunctions/
Mon, 01 Jan 0001 00:00:00 +0000/theories/funwithfunctions/FunWithTilings
/theories/funwithtilings/
Mon, 01 Jan 0001 00:00:00 +0000/theories/funwithtilings/Furstenberg_Topology
/theories/furstenberg_topology/
Mon, 01 Jan 0001 00:00:00 +0000/theories/furstenberg_topology/Gabow_SCC
/theories/gabow_scc/
Mon, 01 Jan 0001 00:00:00 +0000/theories/gabow_scc/Gale_Shapley
/theories/gale_shapley/
Mon, 01 Jan 0001 00:00:00 +0000/theories/gale_shapley/GaleStewart_Games
/theories/galestewart_games/
Mon, 01 Jan 0001 00:00:00 +0000/theories/galestewart_games/Game_Based_Crypto
/theories/game_based_crypto/
Mon, 01 Jan 0001 00:00:00 +0000/theories/game_based_crypto/Gauss-Jordan-Elim-Fun
/theories/gauss-jordan-elim-fun/
Mon, 01 Jan 0001 00:00:00 +0000/theories/gauss-jordan-elim-fun/Gauss_Jordan
/theories/gauss_jordan/
Mon, 01 Jan 0001 00:00:00 +0000/theories/gauss_jordan/Gauss_Sums
/theories/gauss_sums/
Mon, 01 Jan 0001 00:00:00 +0000/theories/gauss_sums/Gaussian_Integers
/theories/gaussian_integers/
Mon, 01 Jan 0001 00:00:00 +0000/theories/gaussian_integers/GenClock
/theories/genclock/
Mon, 01 Jan 0001 00:00:00 +0000/theories/genclock/General-Triangle
/theories/general-triangle/
Mon, 01 Jan 0001 00:00:00 +0000/theories/general-triangle/Generalized_Counting_Sort
/theories/generalized_counting_sort/
Mon, 01 Jan 0001 00:00:00 +0000/theories/generalized_counting_sort/Generic_Deriving
/theories/generic_deriving/
Mon, 01 Jan 0001 00:00:00 +0000/theories/generic_deriving/Generic_Join
/theories/generic_join/
Mon, 01 Jan 0001 00:00:00 +0000/theories/generic_join/GewirthPGCProof
/theories/gewirthpgcproof/
Mon, 01 Jan 0001 00:00:00 +0000/theories/gewirthpgcproof/Girth_Chromatic
/theories/girth_chromatic/
Mon, 01 Jan 0001 00:00:00 +0000/theories/girth_chromatic/Goedel_HFSet_Semantic
/theories/goedel_hfset_semantic/
Mon, 01 Jan 0001 00:00:00 +0000/theories/goedel_hfset_semantic/Goedel_HFSet_Semanticless
/theories/goedel_hfset_semanticless/
Mon, 01 Jan 0001 00:00:00 +0000/theories/goedel_hfset_semanticless/Goedel_Incompleteness
/theories/goedel_incompleteness/
Mon, 01 Jan 0001 00:00:00 +0000/theories/goedel_incompleteness/GoedelGod
/theories/goedelgod/
Mon, 01 Jan 0001 00:00:00 +0000/theories/goedelgod/Goodstein_Lambda
/theories/goodstein_lambda/
Mon, 01 Jan 0001 00:00:00 +0000/theories/goodstein_lambda/GPU_Kernel_PL
/theories/gpu_kernel_pl/
Mon, 01 Jan 0001 00:00:00 +0000/theories/gpu_kernel_pl/Graph_Saturation
/theories/graph_saturation/
Mon, 01 Jan 0001 00:00:00 +0000/theories/graph_saturation/Graph_Theory
/theories/graph_theory/
Mon, 01 Jan 0001 00:00:00 +0000/theories/graph_theory/GraphMarkingIBP
/theories/graphmarkingibp/
Mon, 01 Jan 0001 00:00:00 +0000/theories/graphmarkingibp/Green
/theories/green/
Mon, 01 Jan 0001 00:00:00 +0000/theories/green/Groebner_Bases
/theories/groebner_bases/
Mon, 01 Jan 0001 00:00:00 +0000/theories/groebner_bases/Groebner_Macaulay
/theories/groebner_macaulay/
Mon, 01 Jan 0001 00:00:00 +0000/theories/groebner_macaulay/Gromov_Hyperbolicity
/theories/gromov_hyperbolicity/
Mon, 01 Jan 0001 00:00:00 +0000/theories/gromov_hyperbolicity/Grothendieck_Schemes
/theories/grothendieck_schemes/
Mon, 01 Jan 0001 00:00:00 +0000/theories/grothendieck_schemes/Group-Ring-Module
/theories/group-ring-module/
Mon, 01 Jan 0001 00:00:00 +0000/theories/group-ring-module/Hahn_Jordan_Decomposition
/theories/hahn_jordan_decomposition/
Mon, 01 Jan 0001 00:00:00 +0000/theories/hahn_jordan_decomposition/Heard_Of
/theories/heard_of/
Mon, 01 Jan 0001 00:00:00 +0000/theories/heard_of/Hello_World
/theories/hello_world/
Mon, 01 Jan 0001 00:00:00 +0000/theories/hello_world/Help
/help/
Mon, 01 Jan 0001 00:00:00 +0000/help/This section focuses on the Archive of Formal Proofs. For help with Isabelle, see the Isabelle Wiki and Documentation
Referring to AFP Entries in Isabelle/JEdit Once you have downloaded the AFP, you can include its articles and theories in your own developments. If you would like to make your work available to others without having to include the AFP articles you depend on, here is how to do it.
-From Isabelle2021 on, the recommended method for making the whole AFP available to Isabelle is the isabelle components -u command.
+From Isabelle2021-1 on, the recommended method for making the whole AFP available to Isabelle is the isabelle components -u command.
HereditarilyFinite
/theories/hereditarilyfinite/
Mon, 01 Jan 0001 00:00:00 +0000/theories/hereditarilyfinite/Hermite
/theories/hermite/
Mon, 01 Jan 0001 00:00:00 +0000/theories/hermite/Hermite_Lindemann
/theories/hermite_lindemann/
Mon, 01 Jan 0001 00:00:00 +0000/theories/hermite_lindemann/Hidden_Markov_Models
/theories/hidden_markov_models/
Mon, 01 Jan 0001 00:00:00 +0000/theories/hidden_markov_models/Higher_Order_Terms
/theories/higher_order_terms/
Mon, 01 Jan 0001 00:00:00 +0000/theories/higher_order_terms/Hoare_Time
/theories/hoare_time/
Mon, 01 Jan 0001 00:00:00 +0000/theories/hoare_time/HOL-CSP
/theories/hol-csp/
Mon, 01 Jan 0001 00:00:00 +0000/theories/hol-csp/HOL-ODE-ARCH-COMP
/theories/hol-ode-arch-comp/
Mon, 01 Jan 0001 00:00:00 +0000/theories/hol-ode-arch-comp/HOL-ODE-Examples
/theories/hol-ode-examples/
Mon, 01 Jan 0001 00:00:00 +0000/theories/hol-ode-examples/HOL-ODE-Numerics
/theories/hol-ode-numerics/
Mon, 01 Jan 0001 00:00:00 +0000/theories/hol-ode-numerics/HOLCF-Prelude
/theories/holcf-prelude/
Mon, 01 Jan 0001 00:00:00 +0000/theories/holcf-prelude/Hood_Melville_Queue
/theories/hood_melville_queue/
Mon, 01 Jan 0001 00:00:00 +0000/theories/hood_melville_queue/HotelKeyCards
/theories/hotelkeycards/
Mon, 01 Jan 0001 00:00:00 +0000/theories/hotelkeycards/HRB-Slicing
/theories/hrb-slicing/
Mon, 01 Jan 0001 00:00:00 +0000/theories/hrb-slicing/Huffman
/theories/huffman/
Mon, 01 Jan 0001 00:00:00 +0000/theories/huffman/Hybrid_Logic
/theories/hybrid_logic/
Mon, 01 Jan 0001 00:00:00 +0000/theories/hybrid_logic/Hybrid_Multi_Lane_Spatial_Logic
/theories/hybrid_multi_lane_spatial_logic/
Mon, 01 Jan 0001 00:00:00 +0000/theories/hybrid_multi_lane_spatial_logic/Hybrid_Systems_VCs
/theories/hybrid_systems_vcs/
Mon, 01 Jan 0001 00:00:00 +0000/theories/hybrid_systems_vcs/HyperCTL
/theories/hyperctl/
Mon, 01 Jan 0001 00:00:00 +0000/theories/hyperctl/Hyperdual
/theories/hyperdual/
Mon, 01 Jan 0001 00:00:00 +0000/theories/hyperdual/IEEE_Floating_Point
/theories/ieee_floating_point/
Mon, 01 Jan 0001 00:00:00 +0000/theories/ieee_floating_point/IFC_Tracking
/theories/ifc_tracking/
Mon, 01 Jan 0001 00:00:00 +0000/theories/ifc_tracking/IMAP-CRDT
/theories/imap-crdt/
Mon, 01 Jan 0001 00:00:00 +0000/theories/imap-crdt/IMO2019
/theories/imo2019/
Mon, 01 Jan 0001 00:00:00 +0000/theories/imo2019/IMP2
/theories/imp2/
Mon, 01 Jan 0001 00:00:00 +0000/theories/imp2/IMP2_Binary_Heap
/theories/imp2_binary_heap/
Mon, 01 Jan 0001 00:00:00 +0000/theories/imp2_binary_heap/IMP_Compiler
/theories/imp_compiler/
Mon, 01 Jan 0001 00:00:00 +0000/theories/imp_compiler/Imperative_Insertion_Sort
/theories/imperative_insertion_sort/
Mon, 01 Jan 0001 00:00:00 +0000/theories/imperative_insertion_sort/Impossible_Geometry
/theories/impossible_geometry/
Mon, 01 Jan 0001 00:00:00 +0000/theories/impossible_geometry/Incompleteness
/theories/incompleteness/
Mon, 01 Jan 0001 00:00:00 +0000/theories/incompleteness/Incredible_Proof_Machine
/theories/incredible_proof_machine/
Mon, 01 Jan 0001 00:00:00 +0000/theories/incredible_proof_machine/Independence_CH
/theories/independence_ch/
Mon, 01 Jan 0001 00:00:00 +0000/theories/independence_ch/Inductive_Confidentiality
/theories/inductive_confidentiality/
Mon, 01 Jan 0001 00:00:00 +0000/theories/inductive_confidentiality/Inductive_Inference
/theories/inductive_inference/
Mon, 01 Jan 0001 00:00:00 +0000/theories/inductive_inference/InformationFlowSlicing
/theories/informationflowslicing/
Mon, 01 Jan 0001 00:00:00 +0000/theories/informationflowslicing/InformationFlowSlicing_Inter
/theories/informationflowslicing_inter/
Mon, 01 Jan 0001 00:00:00 +0000/theories/informationflowslicing_inter/InfPathElimination
/theories/infpathelimination/
Mon, 01 Jan 0001 00:00:00 +0000/theories/infpathelimination/Integration
/theories/integration/
Mon, 01 Jan 0001 00:00:00 +0000/theories/integration/Interpolation_Polynomials_HOL_Algebra
/theories/interpolation_polynomials_hol_algebra/
Mon, 01 Jan 0001 00:00:00 +0000/theories/interpolation_polynomials_hol_algebra/Interpreter_Optimizations
/theories/interpreter_optimizations/
Mon, 01 Jan 0001 00:00:00 +0000/theories/interpreter_optimizations/Interval_Arithmetic_Word32
/theories/interval_arithmetic_word32/
Mon, 01 Jan 0001 00:00:00 +0000/theories/interval_arithmetic_word32/Intro_Dest_Elim
/theories/intro_dest_elim/
Mon, 01 Jan 0001 00:00:00 +0000/theories/intro_dest_elim/IP_Addresses
/theories/ip_addresses/
Mon, 01 Jan 0001 00:00:00 +0000/theories/ip_addresses/Iptables_Semantics
/theories/iptables_semantics/
Mon, 01 Jan 0001 00:00:00 +0000/theories/iptables_semantics/Iptables_Semantics_Examples
/theories/iptables_semantics_examples/
Mon, 01 Jan 0001 00:00:00 +0000/theories/iptables_semantics_examples/Iptables_Semantics_Examples_Big
/theories/iptables_semantics_examples_big/
Mon, 01 Jan 0001 00:00:00 +0000/theories/iptables_semantics_examples_big/Irrational_Series_Erdos_Straus
/theories/irrational_series_erdos_straus/
Mon, 01 Jan 0001 00:00:00 +0000/theories/irrational_series_erdos_straus/Irrationality_J_Hancl
/theories/irrationality_j_hancl/
Mon, 01 Jan 0001 00:00:00 +0000/theories/irrationality_j_hancl/Irrationals_From_THEBOOK
/theories/irrationals_from_thebook/
Mon, 01 Jan 0001 00:00:00 +0000/theories/irrationals_from_thebook/Isabelle_C
/theories/isabelle_c/
Mon, 01 Jan 0001 00:00:00 +0000/theories/isabelle_c/Isabelle_Marries_Dirac
/theories/isabelle_marries_dirac/
Mon, 01 Jan 0001 00:00:00 +0000/theories/isabelle_marries_dirac/Isabelle_Meta_Model
/theories/isabelle_meta_model/
Mon, 01 Jan 0001 00:00:00 +0000/theories/isabelle_meta_model/IsaGeoCoq
/theories/isageocoq/
Mon, 01 Jan 0001 00:00:00 +0000/theories/isageocoq/Jacobson_Basic_Algebra
/theories/jacobson_basic_algebra/
Mon, 01 Jan 0001 00:00:00 +0000/theories/jacobson_basic_algebra/Jinja
/theories/jinja/
Mon, 01 Jan 0001 00:00:00 +0000/theories/jinja/JinjaDCI
/theories/jinjadci/
Mon, 01 Jan 0001 00:00:00 +0000/theories/jinjadci/JinjaThreads
/theories/jinjathreads/
Mon, 01 Jan 0001 00:00:00 +0000/theories/jinjathreads/JiveDataStoreModel
/theories/jivedatastoremodel/
Mon, 01 Jan 0001 00:00:00 +0000/theories/jivedatastoremodel/Jordan_Hoelder
/theories/jordan_hoelder/
Mon, 01 Jan 0001 00:00:00 +0000/theories/jordan_hoelder/Jordan_Normal_Form
/theories/jordan_normal_form/
Mon, 01 Jan 0001 00:00:00 +0000/theories/jordan_normal_form/KAD
/theories/kad/
Mon, 01 Jan 0001 00:00:00 +0000/theories/kad/KAT_and_DRA
/theories/kat_and_dra/
Mon, 01 Jan 0001 00:00:00 +0000/theories/kat_and_dra/KBPs
/theories/kbps/
Mon, 01 Jan 0001 00:00:00 +0000/theories/kbps/KD_Tree
/theories/kd_tree/
Mon, 01 Jan 0001 00:00:00 +0000/theories/kd_tree/Key_Agreement_Strong_Adversaries
/theories/key_agreement_strong_adversaries/
Mon, 01 Jan 0001 00:00:00 +0000/theories/key_agreement_strong_adversaries/Kleene_Algebra
/theories/kleene_algebra/
Mon, 01 Jan 0001 00:00:00 +0000/theories/kleene_algebra/Knights_Tour
/theories/knights_tour/
Mon, 01 Jan 0001 00:00:00 +0000/theories/knights_tour/Knot_Theory
/theories/knot_theory/
Mon, 01 Jan 0001 00:00:00 +0000/theories/knot_theory/Knuth_Bendix_Order
/theories/knuth_bendix_order/
Mon, 01 Jan 0001 00:00:00 +0000/theories/knuth_bendix_order/Knuth_Morris_Pratt
/theories/knuth_morris_pratt/
Mon, 01 Jan 0001 00:00:00 +0000/theories/knuth_morris_pratt/Koenigsberg_Friendship
/theories/koenigsberg_friendship/
Mon, 01 Jan 0001 00:00:00 +0000/theories/koenigsberg_friendship/Kruskal
/theories/kruskal/
Mon, 01 Jan 0001 00:00:00 +0000/theories/kruskal/Kuratowski_Closure_Complement
/theories/kuratowski_closure_complement/
Mon, 01 Jan 0001 00:00:00 +0000/theories/kuratowski_closure_complement/Lam-ml-Normalization
/theories/lam-ml-normalization/
Mon, 01 Jan 0001 00:00:00 +0000/theories/lam-ml-normalization/Lambda_Free_EPO
/theories/lambda_free_epo/
Mon, 01 Jan 0001 00:00:00 +0000/theories/lambda_free_epo/Lambda_Free_KBOs
/theories/lambda_free_kbos/
Mon, 01 Jan 0001 00:00:00 +0000/theories/lambda_free_kbos/Lambda_Free_RPOs
/theories/lambda_free_rpos/
Mon, 01 Jan 0001 00:00:00 +0000/theories/lambda_free_rpos/LambdaAuth
/theories/lambdaauth/
Mon, 01 Jan 0001 00:00:00 +0000/theories/lambdaauth/LambdaMu
/theories/lambdamu/
Mon, 01 Jan 0001 00:00:00 +0000/theories/lambdamu/Lambert_W
/theories/lambert_w/
Mon, 01 Jan 0001 00:00:00 +0000/theories/lambert_w/Landau_Symbols
/theories/landau_symbols/
Mon, 01 Jan 0001 00:00:00 +0000/theories/landau_symbols/Laplace_Transform
/theories/laplace_transform/
Mon, 01 Jan 0001 00:00:00 +0000/theories/laplace_transform/Latin_Square
/theories/latin_square/
Mon, 01 Jan 0001 00:00:00 +0000/theories/latin_square/LatticeProperties
/theories/latticeproperties/
Mon, 01 Jan 0001 00:00:00 +0000/theories/latticeproperties/Launchbury
/theories/launchbury/
Mon, 01 Jan 0001 00:00:00 +0000/theories/launchbury/Laws_of_Large_Numbers
/theories/laws_of_large_numbers/
Mon, 01 Jan 0001 00:00:00 +0000/theories/laws_of_large_numbers/Lazy-Lists-II
/theories/lazy-lists-ii/
Mon, 01 Jan 0001 00:00:00 +0000/theories/lazy-lists-ii/Lazy_Case
/theories/lazy_case/
Mon, 01 Jan 0001 00:00:00 +0000/theories/lazy_case/Lehmer
/theories/lehmer/
Mon, 01 Jan 0001 00:00:00 +0000/theories/lehmer/LEM
/theories/lem/
Mon, 01 Jan 0001 00:00:00 +0000/theories/lem/Lifting_Definition_Option
/theories/lifting_definition_option/
Mon, 01 Jan 0001 00:00:00 +0000/theories/lifting_definition_option/Lifting_the_Exponent
/theories/lifting_the_exponent/
Mon, 01 Jan 0001 00:00:00 +0000/theories/lifting_the_exponent/LightweightJava
/theories/lightweightjava/
Mon, 01 Jan 0001 00:00:00 +0000/theories/lightweightjava/Linear_Inequalities
/theories/linear_inequalities/
Mon, 01 Jan 0001 00:00:00 +0000/theories/linear_inequalities/Linear_Programming
/theories/linear_programming/
Mon, 01 Jan 0001 00:00:00 +0000/theories/linear_programming/Linear_Recurrences
/theories/linear_recurrences/
Mon, 01 Jan 0001 00:00:00 +0000/theories/linear_recurrences/Linear_Recurrences_Solver
/theories/linear_recurrences_solver/
Mon, 01 Jan 0001 00:00:00 +0000/theories/linear_recurrences_solver/LinearQuantifierElim
/theories/linearquantifierelim/
Mon, 01 Jan 0001 00:00:00 +0000/theories/linearquantifierelim/Liouville_Numbers
/theories/liouville_numbers/
Mon, 01 Jan 0001 00:00:00 +0000/theories/liouville_numbers/List-Index
/theories/list-index/
Mon, 01 Jan 0001 00:00:00 +0000/theories/list-index/List-Infinite
/theories/list-infinite/
Mon, 01 Jan 0001 00:00:00 +0000/theories/list-infinite/List_Interleaving
/theories/list_interleaving/
Mon, 01 Jan 0001 00:00:00 +0000/theories/list_interleaving/List_Inversions
/theories/list_inversions/
Mon, 01 Jan 0001 00:00:00 +0000/theories/list_inversions/List_Update
/theories/list_update/
Mon, 01 Jan 0001 00:00:00 +0000/theories/list_update/LLL_Basis_Reduction
/theories/lll_basis_reduction/
Mon, 01 Jan 0001 00:00:00 +0000/theories/lll_basis_reduction/LLL_Factorization
/theories/lll_factorization/
Mon, 01 Jan 0001 00:00:00 +0000/theories/lll_factorization/Localization_Ring
/theories/localization_ring/
Mon, 01 Jan 0001 00:00:00 +0000/theories/localization_ring/LocalLexing
/theories/locallexing/
Mon, 01 Jan 0001 00:00:00 +0000/theories/locallexing/Locally-Nameless-Sigma
/theories/locally-nameless-sigma/
Mon, 01 Jan 0001 00:00:00 +0000/theories/locally-nameless-sigma/LOFT
/theories/loft/
Mon, 01 Jan 0001 00:00:00 +0000/theories/loft/Logging_Independent_Anonymity
/theories/logging_independent_anonymity/
Mon, 01 Jan 0001 00:00:00 +0000/theories/logging_independent_anonymity/Lorenz_Approximation
/theories/lorenz_approximation/
Mon, 01 Jan 0001 00:00:00 +0000/theories/lorenz_approximation/Lorenz_C0
/theories/lorenz_c0/
Mon, 01 Jan 0001 00:00:00 +0000/theories/lorenz_c0/Lorenz_C1
/theories/lorenz_c1/
Mon, 01 Jan 0001 00:00:00 +0000/theories/lorenz_c1/Lowe_Ontological_Argument
/theories/lowe_ontological_argument/
Mon, 01 Jan 0001 00:00:00 +0000/theories/lowe_ontological_argument/Lower_Semicontinuous
/theories/lower_semicontinuous/
Mon, 01 Jan 0001 00:00:00 +0000/theories/lower_semicontinuous/Lp
/theories/lp/
Mon, 01 Jan 0001 00:00:00 +0000/theories/lp/LP_Duality
/theories/lp_duality/
Mon, 01 Jan 0001 00:00:00 +0000/theories/lp_duality/LTL
/theories/ltl/
Mon, 01 Jan 0001 00:00:00 +0000/theories/ltl/LTL_Master_Theorem
/theories/ltl_master_theorem/
Mon, 01 Jan 0001 00:00:00 +0000/theories/ltl_master_theorem/LTL_Normal_Form
/theories/ltl_normal_form/
Mon, 01 Jan 0001 00:00:00 +0000/theories/ltl_normal_form/LTL_to_DRA
/theories/ltl_to_dra/
Mon, 01 Jan 0001 00:00:00 +0000/theories/ltl_to_dra/LTL_to_GBA
/theories/ltl_to_gba/
Mon, 01 Jan 0001 00:00:00 +0000/theories/ltl_to_gba/Lucas_Theorem
/theories/lucas_theorem/
Mon, 01 Jan 0001 00:00:00 +0000/theories/lucas_theorem/Markov_Models
/theories/markov_models/
Mon, 01 Jan 0001 00:00:00 +0000/theories/markov_models/Marriage
/theories/marriage/
Mon, 01 Jan 0001 00:00:00 +0000/theories/marriage/Mason_Stothers
/theories/mason_stothers/
Mon, 01 Jan 0001 00:00:00 +0000/theories/mason_stothers/Matrices_for_ODEs
/theories/matrices_for_odes/
Mon, 01 Jan 0001 00:00:00 +0000/theories/matrices_for_odes/Matrix
/theories/matrix/
Mon, 01 Jan 0001 00:00:00 +0000/theories/matrix/Matrix_Tensor
/theories/matrix_tensor/
Mon, 01 Jan 0001 00:00:00 +0000/theories/matrix_tensor/Matroids
/theories/matroids/
Mon, 01 Jan 0001 00:00:00 +0000/theories/matroids/Max-Card-Matching
/theories/max-card-matching/
Mon, 01 Jan 0001 00:00:00 +0000/theories/max-card-matching/MDP-Algorithms
/theories/mdp-algorithms/
Mon, 01 Jan 0001 00:00:00 +0000/theories/mdp-algorithms/MDP-Rewards
/theories/mdp-rewards/
Mon, 01 Jan 0001 00:00:00 +0000/theories/mdp-rewards/Median_Method
/theories/median_method/
Mon, 01 Jan 0001 00:00:00 +0000/theories/median_method/Median_Of_Medians_Selection
/theories/median_of_medians_selection/
Mon, 01 Jan 0001 00:00:00 +0000/theories/median_of_medians_selection/Menger
/theories/menger/
Mon, 01 Jan 0001 00:00:00 +0000/theories/menger/Mereology
/theories/mereology/
Mon, 01 Jan 0001 00:00:00 +0000/theories/mereology/Mersenne_Primes
/theories/mersenne_primes/
Mon, 01 Jan 0001 00:00:00 +0000/theories/mersenne_primes/Metalogic_ProofChecker
/theories/metalogic_proofchecker/
Mon, 01 Jan 0001 00:00:00 +0000/theories/metalogic_proofchecker/MFMC_Countable
/theories/mfmc_countable/
Mon, 01 Jan 0001 00:00:00 +0000/theories/mfmc_countable/MFODL_Monitor_Optimized
/theories/mfodl_monitor_optimized/
Mon, 01 Jan 0001 00:00:00 +0000/theories/mfodl_monitor_optimized/MFOTL_Monitor
/theories/mfotl_monitor/
Mon, 01 Jan 0001 00:00:00 +0000/theories/mfotl_monitor/Minimal_SSA
/theories/minimal_ssa/
Mon, 01 Jan 0001 00:00:00 +0000/theories/minimal_ssa/MiniML
/theories/miniml/
Mon, 01 Jan 0001 00:00:00 +0000/theories/miniml/MiniSail
/theories/minisail/
Mon, 01 Jan 0001 00:00:00 +0000/theories/minisail/Minkowskis_Theorem
/theories/minkowskis_theorem/
Mon, 01 Jan 0001 00:00:00 +0000/theories/minkowskis_theorem/Minsky_Machines
/theories/minsky_machines/
Mon, 01 Jan 0001 00:00:00 +0000/theories/minsky_machines/Modal_Logics_for_NTS
/theories/modal_logics_for_nts/
Mon, 01 Jan 0001 00:00:00 +0000/theories/modal_logics_for_nts/Modular_arithmetic_LLL_and_HNF_algorithms
/theories/modular_arithmetic_lll_and_hnf_algorithms/
Mon, 01 Jan 0001 00:00:00 +0000/theories/modular_arithmetic_lll_and_hnf_algorithms/Modular_Assembly_Kit_Security
/theories/modular_assembly_kit_security/
Mon, 01 Jan 0001 00:00:00 +0000/theories/modular_assembly_kit_security/Monad_Memo_DP
/theories/monad_memo_dp/
Mon, 01 Jan 0001 00:00:00 +0000/theories/monad_memo_dp/Monad_Normalisation
/theories/monad_normalisation/
Mon, 01 Jan 0001 00:00:00 +0000/theories/monad_normalisation/MonoBoolTranAlgebra
/theories/monobooltranalgebra/
Mon, 01 Jan 0001 00:00:00 +0000/theories/monobooltranalgebra/MonoidalCategory
/theories/monoidalcategory/
Mon, 01 Jan 0001 00:00:00 +0000/theories/monoidalcategory/Monomorphic_Monad
/theories/monomorphic_monad/
Mon, 01 Jan 0001 00:00:00 +0000/theories/monomorphic_monad/MSO_Regex_Equivalence
/theories/mso_regex_equivalence/
Mon, 01 Jan 0001 00:00:00 +0000/theories/mso_regex_equivalence/MuchAdoAboutTwo
/theories/muchadoabouttwo/
Mon, 01 Jan 0001 00:00:00 +0000/theories/muchadoabouttwo/Multi_Party_Computation
/theories/multi_party_computation/
Mon, 01 Jan 0001 00:00:00 +0000/theories/multi_party_computation/Multirelations
/theories/multirelations/
Mon, 01 Jan 0001 00:00:00 +0000/theories/multirelations/Multiset_Ordering_NPC
/theories/multiset_ordering_npc/
Mon, 01 Jan 0001 00:00:00 +0000/theories/multiset_ordering_npc/Myhill-Nerode
/theories/myhill-nerode/
Mon, 01 Jan 0001 00:00:00 +0000/theories/myhill-nerode/Name_Carrying_Type_Inference
/theories/name_carrying_type_inference/
Mon, 01 Jan 0001 00:00:00 +0000/theories/name_carrying_type_inference/Nash_Williams
/theories/nash_williams/
Mon, 01 Jan 0001 00:00:00 +0000/theories/nash_williams/Nat-Interval-Logic
/theories/nat-interval-logic/
Mon, 01 Jan 0001 00:00:00 +0000/theories/nat-interval-logic/Native_Word
/theories/native_word/
Mon, 01 Jan 0001 00:00:00 +0000/theories/native_word/Nested_Multisets_Ordinals
/theories/nested_multisets_ordinals/
Mon, 01 Jan 0001 00:00:00 +0000/theories/nested_multisets_ordinals/Network_Security_Policy_Verification
/theories/network_security_policy_verification/
Mon, 01 Jan 0001 00:00:00 +0000/theories/network_security_policy_verification/Neumann_Morgenstern_Utility
/theories/neumann_morgenstern_utility/
Mon, 01 Jan 0001 00:00:00 +0000/theories/neumann_morgenstern_utility/No_FTL_observers
/theories/no_ftl_observers/
Mon, 01 Jan 0001 00:00:00 +0000/theories/no_ftl_observers/Nominal2
/theories/nominal2/
Mon, 01 Jan 0001 00:00:00 +0000/theories/nominal2/Noninterference_Concurrent_Composition
/theories/noninterference_concurrent_composition/
Mon, 01 Jan 0001 00:00:00 +0000/theories/noninterference_concurrent_composition/Noninterference_CSP
/theories/noninterference_csp/
Mon, 01 Jan 0001 00:00:00 +0000/theories/noninterference_csp/Noninterference_Generic_Unwinding
/theories/noninterference_generic_unwinding/
Mon, 01 Jan 0001 00:00:00 +0000/theories/noninterference_generic_unwinding/Noninterference_Inductive_Unwinding
/theories/noninterference_inductive_unwinding/
Mon, 01 Jan 0001 00:00:00 +0000/theories/noninterference_inductive_unwinding/Noninterference_Ipurge_Unwinding
/theories/noninterference_ipurge_unwinding/
Mon, 01 Jan 0001 00:00:00 +0000/theories/noninterference_ipurge_unwinding/Noninterference_Sequential_Composition
/theories/noninterference_sequential_composition/
Mon, 01 Jan 0001 00:00:00 +0000/theories/noninterference_sequential_composition/NormByEval
/theories/normbyeval/
Mon, 01 Jan 0001 00:00:00 +0000/theories/normbyeval/Nullstellensatz
/theories/nullstellensatz/
Mon, 01 Jan 0001 00:00:00 +0000/theories/nullstellensatz/Octonions
/theories/octonions/
Mon, 01 Jan 0001 00:00:00 +0000/theories/octonions/Old_Datatype_Show
/theories/old_datatype_show/
Mon, 01 Jan 0001 00:00:00 +0000/theories/old_datatype_show/Open_Induction
/theories/open_induction/
Mon, 01 Jan 0001 00:00:00 +0000/theories/open_induction/OpSets
/theories/opsets/
Mon, 01 Jan 0001 00:00:00 +0000/theories/opsets/Optics
/theories/optics/
Mon, 01 Jan 0001 00:00:00 +0000/theories/optics/Optimal_BST
/theories/optimal_bst/
Mon, 01 Jan 0001 00:00:00 +0000/theories/optimal_bst/Orbit_Stabiliser
/theories/orbit_stabiliser/
Mon, 01 Jan 0001 00:00:00 +0000/theories/orbit_stabiliser/Order_Lattice_Props
/theories/order_lattice_props/
Mon, 01 Jan 0001 00:00:00 +0000/theories/order_lattice_props/Ordered_Resolution_Prover
/theories/ordered_resolution_prover/
Mon, 01 Jan 0001 00:00:00 +0000/theories/ordered_resolution_prover/Ordinal
/theories/ordinal/
Mon, 01 Jan 0001 00:00:00 +0000/theories/ordinal/Ordinal_Partitions
/theories/ordinal_partitions/
Mon, 01 Jan 0001 00:00:00 +0000/theories/ordinal_partitions/Ordinals_and_Cardinals
/theories/ordinals_and_cardinals/
Mon, 01 Jan 0001 00:00:00 +0000/theories/ordinals_and_cardinals/Ordinary_Differential_Equations
/theories/ordinary_differential_equations/
Mon, 01 Jan 0001 00:00:00 +0000/theories/ordinary_differential_equations/PAC_Checker
/theories/pac_checker/
Mon, 01 Jan 0001 00:00:00 +0000/theories/pac_checker/Package_logic
/theories/package_logic/
Mon, 01 Jan 0001 00:00:00 +0000/theories/package_logic/Padic_Ints
/theories/padic_ints/
Mon, 01 Jan 0001 00:00:00 +0000/theories/padic_ints/Pairing_Heap
/theories/pairing_heap/
Mon, 01 Jan 0001 00:00:00 +0000/theories/pairing_heap/PAL
/theories/pal/
Mon, 01 Jan 0001 00:00:00 +0000/theories/pal/Paraconsistency
/theories/paraconsistency/
Mon, 01 Jan 0001 00:00:00 +0000/theories/paraconsistency/Parity_Game
/theories/parity_game/
Mon, 01 Jan 0001 00:00:00 +0000/theories/parity_game/Partial_Function_MR
/theories/partial_function_mr/
Mon, 01 Jan 0001 00:00:00 +0000/theories/partial_function_mr/Partial_Order_Reduction
/theories/partial_order_reduction/
Mon, 01 Jan 0001 00:00:00 +0000/theories/partial_order_reduction/Password_Authentication_Protocol
/theories/password_authentication_protocol/
Mon, 01 Jan 0001 00:00:00 +0000/theories/password_authentication_protocol/PCF
/theories/pcf/
Mon, 01 Jan 0001 00:00:00 +0000/theories/pcf/Pell
/theories/pell/
Mon, 01 Jan 0001 00:00:00 +0000/theories/pell/Perfect-Number-Thm
/theories/perfect-number-thm/
Mon, 01 Jan 0001 00:00:00 +0000/theories/perfect-number-thm/Perron_Frobenius
/theories/perron_frobenius/
Mon, 01 Jan 0001 00:00:00 +0000/theories/perron_frobenius/pGCL
/theories/pgcl/
Mon, 01 Jan 0001 00:00:00 +0000/theories/pgcl/Physical_Quantities
/theories/physical_quantities/
Mon, 01 Jan 0001 00:00:00 +0000/theories/physical_quantities/Pi_Calculus
/theories/pi_calculus/
Mon, 01 Jan 0001 00:00:00 +0000/theories/pi_calculus/Pi_Transcendental
/theories/pi_transcendental/
Mon, 01 Jan 0001 00:00:00 +0000/theories/pi_transcendental/Planarity_Certificates
/theories/planarity_certificates/
Mon, 01 Jan 0001 00:00:00 +0000/theories/planarity_certificates/PLM
/theories/plm/
Mon, 01 Jan 0001 00:00:00 +0000/theories/plm/Pluennecke_Ruzsa_Inequality
/theories/pluennecke_ruzsa_inequality/
Mon, 01 Jan 0001 00:00:00 +0000/theories/pluennecke_ruzsa_inequality/Poincare_Bendixson
/theories/poincare_bendixson/
Mon, 01 Jan 0001 00:00:00 +0000/theories/poincare_bendixson/Poincare_Disc
/theories/poincare_disc/
Mon, 01 Jan 0001 00:00:00 +0000/theories/poincare_disc/Polynomial_Factorization
/theories/polynomial_factorization/
Mon, 01 Jan 0001 00:00:00 +0000/theories/polynomial_factorization/Polynomial_Interpolation
/theories/polynomial_interpolation/
Mon, 01 Jan 0001 00:00:00 +0000/theories/polynomial_interpolation/Polynomials
/theories/polynomials/
Mon, 01 Jan 0001 00:00:00 +0000/theories/polynomials/Pop_Refinement
/theories/pop_refinement/
Mon, 01 Jan 0001 00:00:00 +0000/theories/pop_refinement/POPLmark-deBruijn
/theories/poplmark-debruijn/
Mon, 01 Jan 0001 00:00:00 +0000/theories/poplmark-debruijn/Posix-Lexing
/theories/posix-lexing/
Mon, 01 Jan 0001 00:00:00 +0000/theories/posix-lexing/Possibilistic_Noninterference
/theories/possibilistic_noninterference/
Mon, 01 Jan 0001 00:00:00 +0000/theories/possibilistic_noninterference/Power_Sum_Polynomials
/theories/power_sum_polynomials/
Mon, 01 Jan 0001 00:00:00 +0000/theories/power_sum_polynomials/Pratt_Certificate
/theories/pratt_certificate/
Mon, 01 Jan 0001 00:00:00 +0000/theories/pratt_certificate/Prefix_Free_Code_Combinators
/theories/prefix_free_code_combinators/
Mon, 01 Jan 0001 00:00:00 +0000/theories/prefix_free_code_combinators/Presburger-Automata
/theories/presburger-automata/
Mon, 01 Jan 0001 00:00:00 +0000/theories/presburger-automata/Prim_Dijkstra_Simple
/theories/prim_dijkstra_simple/
Mon, 01 Jan 0001 00:00:00 +0000/theories/prim_dijkstra_simple/Prime_Distribution_Elementary
/theories/prime_distribution_elementary/
Mon, 01 Jan 0001 00:00:00 +0000/theories/prime_distribution_elementary/Prime_Harmonic_Series
/theories/prime_harmonic_series/
Mon, 01 Jan 0001 00:00:00 +0000/theories/prime_harmonic_series/Prime_Number_Theorem
/theories/prime_number_theorem/
Mon, 01 Jan 0001 00:00:00 +0000/theories/prime_number_theorem/Priority_Queue_Braun
/theories/priority_queue_braun/
Mon, 01 Jan 0001 00:00:00 +0000/theories/priority_queue_braun/Priority_Search_Trees
/theories/priority_search_trees/
Mon, 01 Jan 0001 00:00:00 +0000/theories/priority_search_trees/Probabilistic_Noninterference
/theories/probabilistic_noninterference/
Mon, 01 Jan 0001 00:00:00 +0000/theories/probabilistic_noninterference/Probabilistic_Prime_Tests
/theories/probabilistic_prime_tests/
Mon, 01 Jan 0001 00:00:00 +0000/theories/probabilistic_prime_tests/Probabilistic_System_Zoo
/theories/probabilistic_system_zoo/
Mon, 01 Jan 0001 00:00:00 +0000/theories/probabilistic_system_zoo/Probabilistic_Timed_Automata
/theories/probabilistic_timed_automata/
Mon, 01 Jan 0001 00:00:00 +0000/theories/probabilistic_timed_automata/Probabilistic_While
/theories/probabilistic_while/
Mon, 01 Jan 0001 00:00:00 +0000/theories/probabilistic_while/Program-Conflict-Analysis
/theories/program-conflict-analysis/
Mon, 01 Jan 0001 00:00:00 +0000/theories/program-conflict-analysis/Progress_Tracking
/theories/progress_tracking/
Mon, 01 Jan 0001 00:00:00 +0000/theories/progress_tracking/Projective_Geometry
/theories/projective_geometry/
Mon, 01 Jan 0001 00:00:00 +0000/theories/projective_geometry/Projective_Measurements
/theories/projective_measurements/
Mon, 01 Jan 0001 00:00:00 +0000/theories/projective_measurements/Promela
/theories/promela/
Mon, 01 Jan 0001 00:00:00 +0000/theories/promela/Proof_Strategy_Language
/theories/proof_strategy_language/
Mon, 01 Jan 0001 00:00:00 +0000/theories/proof_strategy_language/Propositional_Proof_Systems
/theories/propositional_proof_systems/
Mon, 01 Jan 0001 00:00:00 +0000/theories/propositional_proof_systems/PropResPI
/theories/proprespi/
Mon, 01 Jan 0001 00:00:00 +0000/theories/proprespi/Prpu_Maxflow
/theories/prpu_maxflow/
Mon, 01 Jan 0001 00:00:00 +0000/theories/prpu_maxflow/PSemigroupsConvolution
/theories/psemigroupsconvolution/
Mon, 01 Jan 0001 00:00:00 +0000/theories/psemigroupsconvolution/PseudoHoops
/theories/pseudohoops/
Mon, 01 Jan 0001 00:00:00 +0000/theories/pseudohoops/Psi_Calculi
/theories/psi_calculi/
Mon, 01 Jan 0001 00:00:00 +0000/theories/psi_calculi/Ptolemys_Theorem
/theories/ptolemys_theorem/
Mon, 01 Jan 0001 00:00:00 +0000/theories/ptolemys_theorem/Public_Announcement_Logic
/theories/public_announcement_logic/
Mon, 01 Jan 0001 00:00:00 +0000/theories/public_announcement_logic/QHLProver
/theories/qhlprover/
Mon, 01 Jan 0001 00:00:00 +0000/theories/qhlprover/QR_Decomposition
/theories/qr_decomposition/
Mon, 01 Jan 0001 00:00:00 +0000/theories/qr_decomposition/Quantales
/theories/quantales/
Mon, 01 Jan 0001 00:00:00 +0000/theories/quantales/Quasi_Borel_Spaces
/theories/quasi_borel_spaces/
Mon, 01 Jan 0001 00:00:00 +0000/theories/quasi_borel_spaces/Quaternions
/theories/quaternions/
Mon, 01 Jan 0001 00:00:00 +0000/theories/quaternions/Quick_Sort_Cost
/theories/quick_sort_cost/
Mon, 01 Jan 0001 00:00:00 +0000/theories/quick_sort_cost/Ramsey-Infinite
/theories/ramsey-infinite/
Mon, 01 Jan 0001 00:00:00 +0000/theories/ramsey-infinite/Random_BSTs
/theories/random_bsts/
Mon, 01 Jan 0001 00:00:00 +0000/theories/random_bsts/Random_Graph_Subgraph_Threshold
/theories/random_graph_subgraph_threshold/
Mon, 01 Jan 0001 00:00:00 +0000/theories/random_graph_subgraph_threshold/Randomised_BSTs
/theories/randomised_bsts/
Mon, 01 Jan 0001 00:00:00 +0000/theories/randomised_bsts/Randomised_Social_Choice
/theories/randomised_social_choice/
Mon, 01 Jan 0001 00:00:00 +0000/theories/randomised_social_choice/Rank_Nullity_Theorem
/theories/rank_nullity_theorem/
Mon, 01 Jan 0001 00:00:00 +0000/theories/rank_nullity_theorem/Real_Impl
/theories/real_impl/
Mon, 01 Jan 0001 00:00:00 +0000/theories/real_impl/Real_Power
/theories/real_power/
Mon, 01 Jan 0001 00:00:00 +0000/theories/real_power/Recursion-Addition
/theories/recursion-addition/
Mon, 01 Jan 0001 00:00:00 +0000/theories/recursion-addition/Recursion-Theory-I
/theories/recursion-theory-i/
Mon, 01 Jan 0001 00:00:00 +0000/theories/recursion-theory-i/Refine_Imperative_HOL
/theories/refine_imperative_hol/
Mon, 01 Jan 0001 00:00:00 +0000/theories/refine_imperative_hol/Refine_Monadic
/theories/refine_monadic/
Mon, 01 Jan 0001 00:00:00 +0000/theories/refine_monadic/RefinementReactive
/theories/refinementreactive/
Mon, 01 Jan 0001 00:00:00 +0000/theories/refinementreactive/Regex_Equivalence
/theories/regex_equivalence/
Mon, 01 Jan 0001 00:00:00 +0000/theories/regex_equivalence/Registers
/theories/registers/
Mon, 01 Jan 0001 00:00:00 +0000/theories/registers/Regression_Test_Selection
/theories/regression_test_selection/
Mon, 01 Jan 0001 00:00:00 +0000/theories/regression_test_selection/Regular-Sets
/theories/regular-sets/
Mon, 01 Jan 0001 00:00:00 +0000/theories/regular-sets/Regular_Algebras
/theories/regular_algebras/
Mon, 01 Jan 0001 00:00:00 +0000/theories/regular_algebras/Regular_Tree_Relations
/theories/regular_tree_relations/
Mon, 01 Jan 0001 00:00:00 +0000/theories/regular_tree_relations/Relation_Algebra
/theories/relation_algebra/
Mon, 01 Jan 0001 00:00:00 +0000/theories/relation_algebra/Relational-Incorrectness-Logic
/theories/relational-incorrectness-logic/
Mon, 01 Jan 0001 00:00:00 +0000/theories/relational-incorrectness-logic/Relational_Disjoint_Set_Forests
/theories/relational_disjoint_set_forests/
Mon, 01 Jan 0001 00:00:00 +0000/theories/relational_disjoint_set_forests/Relational_Forests
/theories/relational_forests/
Mon, 01 Jan 0001 00:00:00 +0000/theories/relational_forests/Relational_Method
/theories/relational_method/
Mon, 01 Jan 0001 00:00:00 +0000/theories/relational_method/Relational_Minimum_Spanning_Trees
/theories/relational_minimum_spanning_trees/
Mon, 01 Jan 0001 00:00:00 +0000/theories/relational_minimum_spanning_trees/Relational_Paths
/theories/relational_paths/
Mon, 01 Jan 0001 00:00:00 +0000/theories/relational_paths/Rep_Fin_Groups
/theories/rep_fin_groups/
Mon, 01 Jan 0001 00:00:00 +0000/theories/rep_fin_groups/Residuated_Lattices
/theories/residuated_lattices/
Mon, 01 Jan 0001 00:00:00 +0000/theories/residuated_lattices/ResiduatedTransitionSystem
/theories/residuatedtransitionsystem/
Mon, 01 Jan 0001 00:00:00 +0000/theories/residuatedtransitionsystem/Resolution_FOL
/theories/resolution_fol/
Mon, 01 Jan 0001 00:00:00 +0000/theories/resolution_fol/Rewrite_Properties_Reduction
/theories/rewrite_properties_reduction/
Mon, 01 Jan 0001 00:00:00 +0000/theories/rewrite_properties_reduction/Rewriting_Z
/theories/rewriting_z/
Mon, 01 Jan 0001 00:00:00 +0000/theories/rewriting_z/Ribbon_Proofs
/theories/ribbon_proofs/
Mon, 01 Jan 0001 00:00:00 +0000/theories/ribbon_proofs/RIPEMD-160-SPARK
/theories/ripemd-160-spark/
Mon, 01 Jan 0001 00:00:00 +0000/theories/ripemd-160-spark/Robbins-Conjecture
/theories/robbins-conjecture/
Mon, 01 Jan 0001 00:00:00 +0000/theories/robbins-conjecture/ROBDD
/theories/robdd/
Mon, 01 Jan 0001 00:00:00 +0000/theories/robdd/Robinson_Arithmetic
/theories/robinson_arithmetic/
Mon, 01 Jan 0001 00:00:00 +0000/theories/robinson_arithmetic/Root_Balanced_Tree
/theories/root_balanced_tree/
Mon, 01 Jan 0001 00:00:00 +0000/theories/root_balanced_tree/Roth_Arithmetic_Progressions
/theories/roth_arithmetic_progressions/
Mon, 01 Jan 0001 00:00:00 +0000/theories/roth_arithmetic_progressions/Routing
/theories/routing/
Mon, 01 Jan 0001 00:00:00 +0000/theories/routing/Roy_Floyd_Warshall
/theories/roy_floyd_warshall/
Mon, 01 Jan 0001 00:00:00 +0000/theories/roy_floyd_warshall/RSAPSS
/theories/rsapss/
Mon, 01 Jan 0001 00:00:00 +0000/theories/rsapss/Safe_Distance
/theories/safe_distance/
Mon, 01 Jan 0001 00:00:00 +0000/theories/safe_distance/Safe_OCL
/theories/safe_ocl/
Mon, 01 Jan 0001 00:00:00 +0000/theories/safe_ocl/SATSolverVerification
/theories/satsolververification/
Mon, 01 Jan 0001 00:00:00 +0000/theories/satsolververification/Saturation_Framework
/theories/saturation_framework/
Mon, 01 Jan 0001 00:00:00 +0000/theories/saturation_framework/Saturation_Framework_Extensions
/theories/saturation_framework_extensions/
Mon, 01 Jan 0001 00:00:00 +0000/theories/saturation_framework_extensions/SC_DOM_Components
/theories/sc_dom_components/
Mon, 01 Jan 0001 00:00:00 +0000/theories/sc_dom_components/Schutz_Spacetime
/theories/schutz_spacetime/
Mon, 01 Jan 0001 00:00:00 +0000/theories/schutz_spacetime/SDS_Impossibility
/theories/sds_impossibility/
Mon, 01 Jan 0001 00:00:00 +0000/theories/sds_impossibility/Search the Archive
/search/
Mon, 01 Jan 0001 00:00:00 +0000/search/Secondary_Sylow
/theories/secondary_sylow/
Mon, 01 Jan 0001 00:00:00 +0000/theories/secondary_sylow/Security_Protocol_Refinement
/theories/security_protocol_refinement/
Mon, 01 Jan 0001 00:00:00 +0000/theories/security_protocol_refinement/Selection_Heap_Sort
/theories/selection_heap_sort/
Mon, 01 Jan 0001 00:00:00 +0000/theories/selection_heap_sort/SenSocialChoice
/theories/sensocialchoice/
Mon, 01 Jan 0001 00:00:00 +0000/theories/sensocialchoice/Separata
/theories/separata/
Mon, 01 Jan 0001 00:00:00 +0000/theories/separata/Separation_Algebra
/theories/separation_algebra/
Mon, 01 Jan 0001 00:00:00 +0000/theories/separation_algebra/Separation_Logic_Imperative_HOL
/theories/separation_logic_imperative_hol/
Mon, 01 Jan 0001 00:00:00 +0000/theories/separation_logic_imperative_hol/Sepref_Basic
/theories/sepref_basic/
Mon, 01 Jan 0001 00:00:00 +0000/theories/sepref_basic/Sepref_IICF
/theories/sepref_iicf/
Mon, 01 Jan 0001 00:00:00 +0000/theories/sepref_iicf/Sepref_Prereq
/theories/sepref_prereq/
Mon, 01 Jan 0001 00:00:00 +0000/theories/sepref_prereq/SequentInvertibility
/theories/sequentinvertibility/
Mon, 01 Jan 0001 00:00:00 +0000/theories/sequentinvertibility/Shadow_DOM
/theories/shadow_dom/
Mon, 01 Jan 0001 00:00:00 +0000/theories/shadow_dom/Shadow_SC_DOM
/theories/shadow_sc_dom/
Mon, 01 Jan 0001 00:00:00 +0000/theories/shadow_sc_dom/Shivers-CFA
/theories/shivers-cfa/
Mon, 01 Jan 0001 00:00:00 +0000/theories/shivers-cfa/ShortestPath
/theories/shortestpath/
Mon, 01 Jan 0001 00:00:00 +0000/theories/shortestpath/Show
/theories/show/
Mon, 01 Jan 0001 00:00:00 +0000/theories/show/SIFPL
/theories/sifpl/
Mon, 01 Jan 0001 00:00:00 +0000/theories/sifpl/SIFUM_Type_Systems
/theories/sifum_type_systems/
Mon, 01 Jan 0001 00:00:00 +0000/theories/sifum_type_systems/Sigma_Commit_Crypto
/theories/sigma_commit_crypto/
Mon, 01 Jan 0001 00:00:00 +0000/theories/sigma_commit_crypto/Signature_Groebner
/theories/signature_groebner/
Mon, 01 Jan 0001 00:00:00 +0000/theories/signature_groebner/Simpl
/theories/simpl/
Mon, 01 Jan 0001 00:00:00 +0000/theories/simpl/Simple_Firewall
/theories/simple_firewall/
Mon, 01 Jan 0001 00:00:00 +0000/theories/simple_firewall/Simplex
/theories/simplex/
Mon, 01 Jan 0001 00:00:00 +0000/theories/simplex/Simplicial_complexes_and_boolean_functions
/theories/simplicial_complexes_and_boolean_functions/
Mon, 01 Jan 0001 00:00:00 +0000/theories/simplicial_complexes_and_boolean_functions/SimplifiedOntologicalArgument
/theories/simplifiedontologicalargument/
Mon, 01 Jan 0001 00:00:00 +0000/theories/simplifiedontologicalargument/Skew_Heap
/theories/skew_heap/
Mon, 01 Jan 0001 00:00:00 +0000/theories/skew_heap/Skip_Lists
/theories/skip_lists/
Mon, 01 Jan 0001 00:00:00 +0000/theories/skip_lists/Slicing
/theories/slicing/
Mon, 01 Jan 0001 00:00:00 +0000/theories/slicing/Sliding_Window_Algorithm
/theories/sliding_window_algorithm/
Mon, 01 Jan 0001 00:00:00 +0000/theories/sliding_window_algorithm/SM
/theories/sm/
Mon, 01 Jan 0001 00:00:00 +0000/theories/sm/SM_Base
/theories/sm_base/
Mon, 01 Jan 0001 00:00:00 +0000/theories/sm_base/Smith_Normal_Form
/theories/smith_normal_form/
Mon, 01 Jan 0001 00:00:00 +0000/theories/smith_normal_form/Smooth_Manifolds
/theories/smooth_manifolds/
Mon, 01 Jan 0001 00:00:00 +0000/theories/smooth_manifolds/Sophomores_Dream
/theories/sophomores_dream/
Mon, 01 Jan 0001 00:00:00 +0000/theories/sophomores_dream/Sort_Encodings
/theories/sort_encodings/
Mon, 01 Jan 0001 00:00:00 +0000/theories/sort_encodings/Source_Coding_Theorem
/theories/source_coding_theorem/
Mon, 01 Jan 0001 00:00:00 +0000/theories/source_coding_theorem/SPARCv8
/theories/sparcv8/
Mon, 01 Jan 0001 00:00:00 +0000/theories/sparcv8/SpecCheck
/theories/speccheck/
Mon, 01 Jan 0001 00:00:00 +0000/theories/speccheck/Special_Function_Bounds
/theories/special_function_bounds/
Mon, 01 Jan 0001 00:00:00 +0000/theories/special_function_bounds/Splay_Tree
/theories/splay_tree/
Mon, 01 Jan 0001 00:00:00 +0000/theories/splay_tree/Sqrt_Babylonian
/theories/sqrt_babylonian/
Mon, 01 Jan 0001 00:00:00 +0000/theories/sqrt_babylonian/Stable_Matching
/theories/stable_matching/
Mon, 01 Jan 0001 00:00:00 +0000/theories/stable_matching/Statecharts
/theories/statecharts/
Mon, 01 Jan 0001 00:00:00 +0000/theories/statecharts/Stateful_Protocol_Composition_and_Typing
/theories/stateful_protocol_composition_and_typing/
Mon, 01 Jan 0001 00:00:00 +0000/theories/stateful_protocol_composition_and_typing/Statistics
/statistics/
Mon, 01 Jan 0001 00:00:00 +0000/statistics/685 Entries 421 Authors ~211,300 Lemmas ~3,423,000 Lines of Code Most used AFP articles: Name Used by ? articles 1. List-Index 21 2. Collections 18 3. Show 16 4. Coinductive 12 5. Deriving 12 6. Jordan_Normal_Form 12 7. Polynomial_Factorization 12 8. Regular-Sets 12 9.Stellar_Quorums
/theories/stellar_quorums/
Mon, 01 Jan 0001 00:00:00 +0000/theories/stellar_quorums/Stern_Brocot
/theories/stern_brocot/
Mon, 01 Jan 0001 00:00:00 +0000/theories/stern_brocot/Stewart_Apollonius
/theories/stewart_apollonius/
Mon, 01 Jan 0001 00:00:00 +0000/theories/stewart_apollonius/Stirling_Formula
/theories/stirling_formula/
Mon, 01 Jan 0001 00:00:00 +0000/theories/stirling_formula/Stochastic_Matrices
/theories/stochastic_matrices/
Mon, 01 Jan 0001 00:00:00 +0000/theories/stochastic_matrices/Stone_Algebras
/theories/stone_algebras/
Mon, 01 Jan 0001 00:00:00 +0000/theories/stone_algebras/Stone_Kleene_Relation_Algebras
/theories/stone_kleene_relation_algebras/
Mon, 01 Jan 0001 00:00:00 +0000/theories/stone_kleene_relation_algebras/Stone_Relation_Algebras
/theories/stone_relation_algebras/
Mon, 01 Jan 0001 00:00:00 +0000/theories/stone_relation_algebras/Store_Buffer_Reduction
/theories/store_buffer_reduction/
Mon, 01 Jan 0001 00:00:00 +0000/theories/store_buffer_reduction/Stream-Fusion
/theories/stream-fusion/
Mon, 01 Jan 0001 00:00:00 +0000/theories/stream-fusion/Stream_Fusion_Code
/theories/stream_fusion_code/
Mon, 01 Jan 0001 00:00:00 +0000/theories/stream_fusion_code/Strong_Security
/theories/strong_security/
Mon, 01 Jan 0001 00:00:00 +0000/theories/strong_security/Sturm_Sequences
/theories/sturm_sequences/
Mon, 01 Jan 0001 00:00:00 +0000/theories/sturm_sequences/Sturm_Tarski
/theories/sturm_tarski/
Mon, 01 Jan 0001 00:00:00 +0000/theories/sturm_tarski/Stuttering_Equivalence
/theories/stuttering_equivalence/
Mon, 01 Jan 0001 00:00:00 +0000/theories/stuttering_equivalence/Subresultants
/theories/subresultants/
Mon, 01 Jan 0001 00:00:00 +0000/theories/subresultants/Subset_Boolean_Algebras
/theories/subset_boolean_algebras/
Mon, 01 Jan 0001 00:00:00 +0000/theories/subset_boolean_algebras/SumSquares
/theories/sumsquares/
Mon, 01 Jan 0001 00:00:00 +0000/theories/sumsquares/Sunflowers
/theories/sunflowers/
Mon, 01 Jan 0001 00:00:00 +0000/theories/sunflowers/SuperCalc
/theories/supercalc/
Mon, 01 Jan 0001 00:00:00 +0000/theories/supercalc/Surprise_Paradox
/theories/surprise_paradox/
Mon, 01 Jan 0001 00:00:00 +0000/theories/surprise_paradox/Symmetric_Polynomials
/theories/symmetric_polynomials/
Mon, 01 Jan 0001 00:00:00 +0000/theories/symmetric_polynomials/Syntax_Independent_Logic
/theories/syntax_independent_logic/
Mon, 01 Jan 0001 00:00:00 +0000/theories/syntax_independent_logic/Szemeredi_Regularity
/theories/szemeredi_regularity/
Mon, 01 Jan 0001 00:00:00 +0000/theories/szemeredi_regularity/Szpilrajn
/theories/szpilrajn/
Mon, 01 Jan 0001 00:00:00 +0000/theories/szpilrajn/Tail_Recursive_Functions
/theories/tail_recursive_functions/
Mon, 01 Jan 0001 00:00:00 +0000/theories/tail_recursive_functions/Tarskis_Geometry
/theories/tarskis_geometry/
Mon, 01 Jan 0001 00:00:00 +0000/theories/tarskis_geometry/Taylor_Models
/theories/taylor_models/
Mon, 01 Jan 0001 00:00:00 +0000/theories/taylor_models/TESL_Language
/theories/tesl_language/
Mon, 01 Jan 0001 00:00:00 +0000/theories/tesl_language/Three_Circles
/theories/three_circles/
Mon, 01 Jan 0001 00:00:00 +0000/theories/three_circles/Timed_Automata
/theories/timed_automata/
Mon, 01 Jan 0001 00:00:00 +0000/theories/timed_automata/TLA
/theories/tla/
Mon, 01 Jan 0001 00:00:00 +0000/theories/tla/Topological_Semantics
/theories/topological_semantics/
Mon, 01 Jan 0001 00:00:00 +0000/theories/topological_semantics/Topology
/theories/topology/
Mon, 01 Jan 0001 00:00:00 +0000/theories/topology/TortoiseHare
/theories/tortoisehare/
Mon, 01 Jan 0001 00:00:00 +0000/theories/tortoisehare/Transcendence_Series_Hancl_Rucki
/theories/transcendence_series_hancl_rucki/
Mon, 01 Jan 0001 00:00:00 +0000/theories/transcendence_series_hancl_rucki/Transformer_Semantics
/theories/transformer_semantics/
Mon, 01 Jan 0001 00:00:00 +0000/theories/transformer_semantics/Transition_Systems_and_Automata
/theories/transition_systems_and_automata/
Mon, 01 Jan 0001 00:00:00 +0000/theories/transition_systems_and_automata/Transitive-Closure
/theories/transitive-closure/
Mon, 01 Jan 0001 00:00:00 +0000/theories/transitive-closure/Transitive-Closure-II
/theories/transitive-closure-ii/
Mon, 01 Jan 0001 00:00:00 +0000/theories/transitive-closure-ii/Transitive_Models
/theories/transitive_models/
Mon, 01 Jan 0001 00:00:00 +0000/theories/transitive_models/Treaps
/theories/treaps/
Mon, 01 Jan 0001 00:00:00 +0000/theories/treaps/Tree-Automata
/theories/tree-automata/
Mon, 01 Jan 0001 00:00:00 +0000/theories/tree-automata/Tree_Decomposition
/theories/tree_decomposition/
Mon, 01 Jan 0001 00:00:00 +0000/theories/tree_decomposition/Triangle
/theories/triangle/
Mon, 01 Jan 0001 00:00:00 +0000/theories/triangle/Trie
/theories/trie/
Mon, 01 Jan 0001 00:00:00 +0000/theories/trie/Twelvefold_Way
/theories/twelvefold_way/
Mon, 01 Jan 0001 00:00:00 +0000/theories/twelvefold_way/Tycon
/theories/tycon/
Mon, 01 Jan 0001 00:00:00 +0000/theories/tycon/Types_Tableaus_and_Goedels_God
/theories/types_tableaus_and_goedels_god/
Mon, 01 Jan 0001 00:00:00 +0000/theories/types_tableaus_and_goedels_god/Types_To_Sets_Extension
/theories/types_to_sets_extension/
Mon, 01 Jan 0001 00:00:00 +0000/theories/types_to_sets_extension/Universal_Hash_Families
/theories/universal_hash_families/
Mon, 01 Jan 0001 00:00:00 +0000/theories/universal_hash_families/Universal_Turing_Machine
/theories/universal_turing_machine/
Mon, 01 Jan 0001 00:00:00 +0000/theories/universal_turing_machine/UpDown_Scheme
/theories/updown_scheme/
Mon, 01 Jan 0001 00:00:00 +0000/theories/updown_scheme/UPF
/theories/upf/
Mon, 01 Jan 0001 00:00:00 +0000/theories/upf/UPF_Firewall
/theories/upf_firewall/
Mon, 01 Jan 0001 00:00:00 +0000/theories/upf_firewall/UTP
/theories/utp/
Mon, 01 Jan 0001 00:00:00 +0000/theories/utp/UTP-Toolkit
/theories/utp-toolkit/
Mon, 01 Jan 0001 00:00:00 +0000/theories/utp-toolkit/Valuation
/theories/valuation/
Mon, 01 Jan 0001 00:00:00 +0000/theories/valuation/Van_der_Waerden
/theories/van_der_waerden/
Mon, 01 Jan 0001 00:00:00 +0000/theories/van_der_waerden/Van_Emde_Boas_Trees
/theories/van_emde_boas_trees/
Mon, 01 Jan 0001 00:00:00 +0000/theories/van_emde_boas_trees/VectorSpace
/theories/vectorspace/
Mon, 01 Jan 0001 00:00:00 +0000/theories/vectorspace/VeriComp
/theories/vericomp/
Mon, 01 Jan 0001 00:00:00 +0000/theories/vericomp/Verified-Prover
/theories/verified-prover/
Mon, 01 Jan 0001 00:00:00 +0000/theories/verified-prover/Verified_SAT_Based_AI_Planning
/theories/verified_sat_based_ai_planning/
Mon, 01 Jan 0001 00:00:00 +0000/theories/verified_sat_based_ai_planning/VerifyThis2018
/theories/verifythis2018/
Mon, 01 Jan 0001 00:00:00 +0000/theories/verifythis2018/VerifyThis2019
/theories/verifythis2019/
Mon, 01 Jan 0001 00:00:00 +0000/theories/verifythis2019/Vickrey_Clarke_Groves
/theories/vickrey_clarke_groves/
Mon, 01 Jan 0001 00:00:00 +0000/theories/vickrey_clarke_groves/Virtual_Substitution
/theories/virtual_substitution/
Mon, 01 Jan 0001 00:00:00 +0000/theories/virtual_substitution/VolpanoSmith
/theories/volpanosmith/
Mon, 01 Jan 0001 00:00:00 +0000/theories/volpanosmith/VYDRA_MDL
/theories/vydra_mdl/
Mon, 01 Jan 0001 00:00:00 +0000/theories/vydra_mdl/WebAssembly
/theories/webassembly/
Mon, 01 Jan 0001 00:00:00 +0000/theories/webassembly/Weight_Balanced_Trees
/theories/weight_balanced_trees/
Mon, 01 Jan 0001 00:00:00 +0000/theories/weight_balanced_trees/Weighted_Path_Order
/theories/weighted_path_order/
Mon, 01 Jan 0001 00:00:00 +0000/theories/weighted_path_order/Well_Quasi_Orders
/theories/well_quasi_orders/
Mon, 01 Jan 0001 00:00:00 +0000/theories/well_quasi_orders/Wetzels_Problem
/theories/wetzels_problem/
Mon, 01 Jan 0001 00:00:00 +0000/theories/wetzels_problem/WHATandWHERE_Security
/theories/whatandwhere_security/
Mon, 01 Jan 0001 00:00:00 +0000/theories/whatandwhere_security/Winding_Number_Eval
/theories/winding_number_eval/
Mon, 01 Jan 0001 00:00:00 +0000/theories/winding_number_eval/WOOT_Strong_Eventual_Consistency
/theories/woot_strong_eventual_consistency/
Mon, 01 Jan 0001 00:00:00 +0000/theories/woot_strong_eventual_consistency/Word_Lib
/theories/word_lib/
Mon, 01 Jan 0001 00:00:00 +0000/theories/word_lib/WorkerWrapper
/theories/workerwrapper/
Mon, 01 Jan 0001 00:00:00 +0000/theories/workerwrapper/X86_Semantics
/theories/x86_semantics/
Mon, 01 Jan 0001 00:00:00 +0000/theories/x86_semantics/XML
/theories/xml/
Mon, 01 Jan 0001 00:00:00 +0000/theories/xml/Youngs_Inequality
/theories/youngs_inequality/
Mon, 01 Jan 0001 00:00:00 +0000/theories/youngs_inequality/Zeta_3_Irrational
/theories/zeta_3_irrational/
Mon, 01 Jan 0001 00:00:00 +0000/theories/zeta_3_irrational/Zeta_Function
/theories/zeta_function/
Mon, 01 Jan 0001 00:00:00 +0000/theories/zeta_function/ZFC_in_HOL
/theories/zfc_in_hol/
Mon, 01 Jan 0001 00:00:00 +0000/theories/zfc_in_hol/