diff --git a/web/entries/Farkas.html b/web/entries/Farkas.html --- a/web/entries/Farkas.html +++ b/web/entries/Farkas.html @@ -1,217 +1,217 @@ Farkas' Lemma and Motzkin's Transposition Theorem - Archive of Formal Proofs

 

 

 

Home
About
Submission
Updating Entries
Using Entries
Search
Statistics
Index
Download

 

 

 

Farkas' Lemma and Motzkin's Transposition Theorem

 

Title: Farkas' Lemma and Motzkin's Transposition Theorem
Authors: - Ralph Bottesch, + Ralph Bottesch, Max W. Haslbeck and René Thiemann (rene /dot/ thiemann /at/ uibk /dot/ ac /dot/ at)
Submission date: 2019-01-17
Abstract: We formalize a proof of Motzkin's transposition theorem and Farkas' lemma in Isabelle/HOL. Our proof is based on the formalization of the simplex algorithm which, given a set of linear constraints, either returns a satisfying assignment to the problem or detects unsatisfiability. By reusing facts about the simplex algorithm we show that a set of linear constraints is unsatisfiable if and only if there is a linear combination of the constraints which evaluates to a trivially unsatisfiable inequality.
BibTeX: 
@article{Farkas-AFP,
   author  = {Ralph Bottesch and Max W. Haslbeck and René Thiemann},
   title   = {Farkas' Lemma and Motzkin's Transposition Theorem},
   journal = {Archive of Formal Proofs},
   month   = jan,
   year    = 2019,
   note    = {\url{https://isa-afp.org/entries/Farkas.html},
             Formal proof development},
   ISSN    = {2150-914x},
 }
License: BSD License
Depends on: Jordan_Normal_Form, Simplex
Used by: Linear_Programming

Proof outline
Proof document
Browse theories
Download this entry
Older releases:
\ No newline at end of file diff --git a/web/entries/Hermite.html b/web/entries/Hermite.html --- a/web/entries/Hermite.html +++ b/web/entries/Hermite.html @@ -1,222 +1,222 @@ Hermite Normal Form - Archive of Formal Proofs

 

 

 

Home
About
Submission
Updating Entries
Using Entries
Search
Statistics
Index
Download

 

 

 

Hermite Normal Form

 

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

Proof outline
Proof document
Browse theories
Download this entry
Older releases:
\ No newline at end of file diff --git a/web/entries/Jordan_Normal_Form.html b/web/entries/Jordan_Normal_Form.html --- a/web/entries/Jordan_Normal_Form.html +++ b/web/entries/Jordan_Normal_Form.html @@ -1,254 +1,254 @@ Matrices, Jordan Normal Forms, and Spectral Radius Theory - Archive of Formal Proofs

 

 

 

Home
About
Submission
Updating Entries
Using Entries
Search
Statistics
Index
Download

 

 

 

Matrices, Jordan Normal Forms, and Spectral Radius Theory

 

- +
Title: Matrices, Jordan Normal Forms, and Spectral Radius Theory
Authors: René Thiemann (rene /dot/ thiemann /at/ uibk /dot/ ac /dot/ at) and Akihisa Yamada
Contributor: Alexander Bentkamp (bentkamp /at/ gmail /dot/ com)
Submission date: 2015-08-21
Abstract:

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

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

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

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

Change history: [2016-01-07]: Added Schur-decomposition, Gram-Schmidt orthogonalization, uniqueness of Jordan normal forms
[2018-04-17]: Integrated lemmas from deep-learning AFP-entry of Alexander Bentkamp
BibTeX: 
@article{Jordan_Normal_Form-AFP,
   author  = {René Thiemann and Akihisa Yamada},
   title   = {Matrices, Jordan Normal Forms, and Spectral Radius Theory},
   journal = {Archive of Formal Proofs},
   month   = aug,
   year    = 2015,
   note    = {\url{https://isa-afp.org/entries/Jordan_Normal_Form.html},
             Formal proof development},
   ISSN    = {2150-914x},
 }
License: BSD License
Depends on: Polynomial_Factorization
Used by:Deep_Learning, Farkas, Groebner_Bases, Isabelle_Marries_Dirac, Linear_Programming, Perron_Frobenius, QHLProver, Stochastic_Matrices, Subresultants
Deep_Learning, Farkas, Groebner_Bases, Isabelle_Marries_Dirac, Linear_Programming, Modular_arithmetic_LLL_and_HNF_algorithms, Perron_Frobenius, QHLProver, Stochastic_Matrices, Subresultants

Proof outline
Proof document
Browse theories
Download this entry
Older releases:
\ No newline at end of file diff --git a/web/entries/LLL_Basis_Reduction.html b/web/entries/LLL_Basis_Reduction.html --- a/web/entries/LLL_Basis_Reduction.html +++ b/web/entries/LLL_Basis_Reduction.html @@ -1,236 +1,236 @@ A verified LLL algorithm - Archive of Formal Proofs

 

 

 

Home
About
Submission
Updating Entries
Using Entries
Search
Statistics
Index
Download

 

 

 

A verified LLL algorithm

 

- +
Title: A verified LLL algorithm
Authors: - Ralph Bottesch, + Ralph Bottesch, Jose Divasón, Maximilian Haslbeck, Sebastiaan Joosten, René Thiemann (rene /dot/ thiemann /at/ uibk /dot/ ac /dot/ at) and Akihisa Yamada
Submission date: 2018-02-02
Abstract: The Lenstra-Lenstra-Lovász basis reduction algorithm, also known as LLL algorithm, is an algorithm to find a basis with short, nearly orthogonal vectors of an integer lattice. Thereby, it can also be seen as an approximation to solve the shortest vector problem (SVP), which is an NP-hard problem, where the approximation quality solely depends on the dimension of the lattice, but not the lattice itself. The algorithm also possesses many applications in diverse fields of computer science, from cryptanalysis to number theory, but it is specially well-known since it was used to implement the first polynomial-time algorithm to factor polynomials. In this work we present the first mechanized soundness proof of the LLL algorithm to compute short vectors in lattices. The formalization follows a textbook by von zur Gathen and Gerhard.
Change history: [2018-04-16]: Integrated formal complexity bounds (Haslbeck, Thiemann) [2018-05-25]: Integrated much faster LLL implementation based on integer arithmetic (Bottesch, Haslbeck, Thiemann)
BibTeX: 
@article{LLL_Basis_Reduction-AFP,
   author  = {Ralph Bottesch and Jose Divasón and Maximilian Haslbeck and Sebastiaan Joosten and René Thiemann and Akihisa Yamada},
   title   = {A verified LLL algorithm},
   journal = {Archive of Formal Proofs},
   month   = feb,
   year    = 2018,
   note    = {\url{https://isa-afp.org/entries/LLL_Basis_Reduction.html},
             Formal proof development},
   ISSN    = {2150-914x},
 }
License: BSD License
Depends on: Algebraic_Numbers, Berlekamp_Zassenhaus
Used by:Linear_Inequalities, LLL_Factorization
Linear_Inequalities, LLL_Factorization, Modular_arithmetic_LLL_and_HNF_algorithms

Proof outline
Proof document
Browse theories
Download this entry
Older releases:
\ No newline at end of file diff --git a/web/entries/Linear_Inequalities.html b/web/entries/Linear_Inequalities.html --- a/web/entries/Linear_Inequalities.html +++ b/web/entries/Linear_Inequalities.html @@ -1,204 +1,204 @@ Linear Inequalities - Archive of Formal Proofs

 

 

 

Home
About
Submission
Updating Entries
Using Entries
Search
Statistics
Index
Download

 

 

 

Linear Inequalities

 

Title: Linear Inequalities
Authors: - Ralph Bottesch, + Ralph Bottesch, Alban Reynaud and René Thiemann (rene /dot/ thiemann /at/ uibk /dot/ ac /dot/ at)
Submission date: 2019-06-21
Abstract: We formalize results about linear inqualities, mainly from Schrijver's book. The main results are the proof of the fundamental theorem on linear inequalities, Farkas' lemma, Carathéodory's theorem, the Farkas-Minkowsky-Weyl theorem, the decomposition theorem of polyhedra, and Meyer's result that the integer hull of a polyhedron is a polyhedron itself. Several theorems include bounds on the appearing numbers, and in particular we provide an a-priori bound on mixed-integer solutions of linear inequalities.
BibTeX: 
@article{Linear_Inequalities-AFP,
   author  = {Ralph Bottesch and Alban Reynaud and René Thiemann},
   title   = {Linear Inequalities},
   journal = {Archive of Formal Proofs},
   month   = jun,
   year    = 2019,
   note    = {\url{https://isa-afp.org/entries/Linear_Inequalities.html},
             Formal proof development},
   ISSN    = {2150-914x},
 }
License: BSD License
Depends on: LLL_Basis_Reduction
Used by: Linear_Programming

Proof outline
Proof document
Browse theories
Download this entry
Older releases:
\ No newline at end of file diff --git a/web/entries/Modular_arithmetic_LLL_and_HNF_algorithms.html b/web/entries/Modular_arithmetic_LLL_and_HNF_algorithms.html new file mode 100644 --- /dev/null +++ b/web/entries/Modular_arithmetic_LLL_and_HNF_algorithms.html @@ -0,0 +1,219 @@ + + + + +Two algorithms based on modular arithmetic: lattice basis reduction and Hermite normal form computation - Archive of Formal Proofs + + + + + + + + + + + + + + + + + + + + + + + + +
+

 

+ + + +

 

+

 

+ + + + + + + + + + + + + + + + + + + + + + + + + + + + +
Home
About
Submission
Updating Entries
Using Entries
Search
Statistics
Index
Download
+

 

+

 

+		 +
+

 

+

Two + + algorithms + + based + + on + + modular + + arithmetic: + + lattice + + basis + + reduction + + and + + Hermite + + normal + + form + + computation + +

+

 

+ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
Title:Two algorithms based on modular arithmetic: lattice basis reduction and Hermite normal form computation
+ Authors: + + Ralph Bottesch, + Jose Divason and + Rene Thiemann +
Submission date:2021-03-12
Abstract: +We verify two algorithms for which modular arithmetic plays an +essential role: Storjohann's variant of the LLL lattice basis +reduction algorithm and Kopparty's algorithm for computing the +Hermite normal form of a matrix. To do this, we also formalize some +facts about the modulo operation with symmetric range. Our +implementations are based on the original papers, but are otherwise +efficient. For basis reduction we formalize two versions: one that +includes all of the optimizations/heuristics from Storjohann's +paper, and one excluding a heuristic that we observed to often +decrease efficiency. We also provide a fast, self-contained certifier +for basis reduction, based on the efficient Hermite normal form +algorithm.
BibTeX: + 
@article{Modular_arithmetic_LLL_and_HNF_algorithms-AFP,
+  author  = {Ralph Bottesch and Jose Divason and Rene Thiemann},
+  title   = {Two algorithms based on modular arithmetic: lattice basis reduction and Hermite normal form computation},
+  journal = {Archive of Formal Proofs},
+  month   = mar,
+  year    = 2021,
+  note    = {\url{https://isa-afp.org/entries/Modular_arithmetic_LLL_and_HNF_algorithms.html},
+            Formal proof development},
+  ISSN    = {2150-914x},
+}
+
License:BSD License
Depends on:Hermite, Jordan_Normal_Form, LLL_Basis_Reduction, Show, Smith_Normal_Form
+ +

+ + + + + + + + + + + + + + + + +
+ Proof outline
+ Proof document +
+ Browse theories +
+ Download this entry +
Older releases: + None +
+ +
+
+ + + + + + \ No newline at end of file diff --git a/web/entries/Show.html b/web/entries/Show.html --- a/web/entries/Show.html +++ b/web/entries/Show.html @@ -1,247 +1,247 @@ Haskell's Show Class in Isabelle/HOL - Archive of Formal Proofs

 

 

 

Home
About
Submission
Updating Entries
Using Entries
Search
Statistics
Index
Download

 

 

 

Haskell's Show Class in Isabelle/HOL

 

- +
Title: Haskell's Show Class in Isabelle/HOL
Authors: Christian Sternagel (c /dot/ sternagel /at/ gmail /dot/ com) and René Thiemann (rene /dot/ thiemann /at/ uibk /dot/ ac /dot/ at)
Submission date: 2014-07-29
Abstract: We implemented a type class for "to-string" functions, similar to Haskell's Show class. Moreover, we provide instantiations for Isabelle/HOL's standard types like bool, prod, sum, nats, ints, and rats. It is further possible, to automatically derive show functions for arbitrary user defined datatypes similar to Haskell's "deriving Show".
Change history: [2015-03-11]: Adapted development to new-style (BNF-based) datatypes.
[2015-04-10]: Moved development for old-style datatypes into subdirectory "Old_Datatype".
BibTeX: 
@article{Show-AFP,
   author  = {Christian Sternagel and René Thiemann},
   title   = {Haskell's Show Class in Isabelle/HOL},
   journal = {Archive of Formal Proofs},
   month   = jul,
   year    = 2014,
   note    = {\url{https://isa-afp.org/entries/Show.html},
             Formal proof development},
   ISSN    = {2150-914x},
 }
License: GNU Lesser General Public License (LGPL)
Depends on: Deriving
Used by:Affine_Arithmetic, AI_Planning_Languages_Semantics, CakeML, CakeML_Codegen, Certification_Monads, Dict_Construction, Monad_Memo_DP, Polynomial_Factorization, Polynomials, Real_Impl, XML
Affine_Arithmetic, AI_Planning_Languages_Semantics, CakeML, CakeML_Codegen, Certification_Monads, Dict_Construction, Modular_arithmetic_LLL_and_HNF_algorithms, Monad_Memo_DP, Polynomial_Factorization, Polynomials, Real_Impl, XML

Proof outline
Proof document
Browse theories
Download this entry
Older releases:
\ No newline at end of file diff --git a/web/entries/Smith_Normal_Form.html b/web/entries/Smith_Normal_Form.html --- a/web/entries/Smith_Normal_Form.html +++ b/web/entries/Smith_Normal_Form.html @@ -1,220 +1,222 @@ A verified algorithm for computing the Smith normal form of a matrix - Archive of Formal Proofs

 

 

 

Home
About
Submission
Updating Entries
Using Entries
Search
Statistics
Index
Download

 

 

 

A verified algorithm for computing the Smith normal form of a matrix

 

- + + +
Title: A verified algorithm for computing the Smith normal form of a matrix
Author: Jose Divasón
Submission date: 2020-05-23
Abstract: This work presents a formal proof in Isabelle/HOL of an algorithm to transform a matrix into its Smith normal form, a canonical matrix form, in a general setting: the algorithm is parameterized by operations to prove its existence over elementary divisor rings, while execution is guaranteed over Euclidean domains. We also provide a formal proof on some results about the generality of this algorithm as well as the uniqueness of the Smith normal form. Since Isabelle/HOL does not feature dependent types, the development is carried out switching conveniently between two different existing libraries: the Hermite normal form (based on HOL Analysis) and the Jordan normal form AFP entries. This permits to reuse results from both developments and it is done by means of the lifting and transfer package together with the use of local type definitions.
BibTeX: 
@article{Smith_Normal_Form-AFP,
   author  = {Jose Divasón},
   title   = {A verified algorithm for computing the Smith normal form of a matrix},
   journal = {Archive of Formal Proofs},
   month   = may,
   year    = 2020,
   note    = {\url{https://isa-afp.org/entries/Smith_Normal_Form.html},
             Formal proof development},
   ISSN    = {2150-914x},
 }
License: BSD License
Depends on: Berlekamp_Zassenhaus, Hermite, List-Index, Perron_Frobenius
Used by:Modular_arithmetic_LLL_and_HNF_algorithms

Proof outline
Proof document
Browse theories
Download this entry
Older releases:
\ No newline at end of file diff --git a/web/index.html b/web/index.html --- a/web/index.html +++ b/web/index.html @@ -1,5388 +1,5398 @@ Archive of Formal Proofs

 

 

 

Home
About
Submission
Updating Entries
Using Entries
Search
Statistics
Index
Download

 

 

 

Archive of Formal Proofs

 

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, is indexed by dblp and has an ISSN: 2150-914x. Submissions are refereed. The preferred citation style is available [here]. We encourage companion AFP submissions to conference and journal publications.

A development version of the archive is available as well.

 

 

+ + +
2021
+ 2021-03-12: Two algorithms based on modular arithmetic: lattice basis reduction and Hermite normal form computation +
+ Authors: + Ralph Bottesch, + Jose Divason + and Rene Thiemann +
2021-03-03: Quantum projective measurements and the CHSH inequality
Author: Mnacho Echenim
2021-03-03: The Hermite–Lindemann–Weierstraß Transcendence Theorem
Author: Manuel Eberl
2021-03-01: Mereology
Author: Ben Blumson
2021-02-25: The Sunflower Lemma of Erdős and Rado
Author: René Thiemann
2021-02-24: A Verified Imperative Implementation of B-Trees
Author: Niels Mündler
2021-02-17: Formal Puiseux Series
Author: Manuel Eberl
2021-02-10: The Laws of Large Numbers
Author: Manuel Eberl
2021-01-31: Tarski's Parallel Postulate implies the 5th Postulate of Euclid, the Postulate of Playfair and the original Parallel Postulate of Euclid
Author: Roland Coghetto
2021-01-30: Solution to the xkcd Blue Eyes puzzle
Author: Jakub Kądziołka
2021-01-18: Hood-Melville Queue
Author: Alejandro Gómez-Londoño
2021-01-11: JinjaDCI: a Java semantics with dynamic class initialization
Author: Susannah Mansky

 

2020
2020-12-27: Cofinality and the Delta System Lemma
Author: Pedro Sánchez Terraf
2020-12-17: Topological semantics for paraconsistent and paracomplete logics
Author: David Fuenmayor
2020-12-08: Relational Minimum Spanning Tree Algorithms
Authors: Walter Guttmann and Nicolas Robinson-O'Brien
2020-12-07: Inline Caching and Unboxing Optimization for Interpreters
Author: Martin Desharnais
2020-12-05: The Relational Method with Message Anonymity for the Verification of Cryptographic Protocols
Author: Pasquale Noce
2020-11-22: Isabelle Marries Dirac: a Library for Quantum Computation and Quantum Information
Authors: Anthony Bordg, Hanna Lachnitt and Yijun He
2020-11-19: The HOL-CSP Refinement Toolkit
Authors: Safouan Taha, Burkhart Wolff and Lina Ye
2020-10-29: Verified SAT-Based AI Planning
Authors: Mohammad Abdulaziz and Friedrich Kurz
2020-10-29: AI Planning Languages Semantics
Authors: Mohammad Abdulaziz and Peter Lammich
2020-10-20: A Sound Type System for Physical Quantities, Units, and Measurements
Authors: Simon Foster and Burkhart Wolff
2020-10-12: Finite Map Extras
Author: Javier Díaz
2020-09-28: A Formal Model of the Safely Composable Document Object Model with Shadow Roots
Authors: Achim D. Brucker and Michael Herzberg
2020-09-28: A Formal Model of the Document Object Model with Shadow Roots
Authors: Achim D. Brucker and Michael Herzberg
2020-09-28: A Formalization of Safely Composable Web Components
Authors: Achim D. Brucker and Michael Herzberg
2020-09-28: A Formalization of Web Components
Authors: Achim D. Brucker and Michael Herzberg
2020-09-28: The Safely Composable DOM
Authors: Achim D. Brucker and Michael Herzberg
2020-09-16: Syntax-Independent Logic Infrastructure
Authors: Andrei Popescu and Dmitriy Traytel
2020-09-16: Robinson Arithmetic
Authors: Andrei Popescu and Dmitriy Traytel
2020-09-16: An Abstract Formalization of Gödel's Incompleteness Theorems
Authors: Andrei Popescu and Dmitriy Traytel
2020-09-16: From Abstract to Concrete Gödel's Incompleteness Theorems—Part II
Authors: Andrei Popescu and Dmitriy Traytel
2020-09-16: From Abstract to Concrete Gödel's Incompleteness Theorems—Part I
Authors: Andrei Popescu and Dmitriy Traytel
2020-09-07: A Formal Model of Extended Finite State Machines
Authors: Michael Foster, Achim D. Brucker, Ramsay G. Taylor and John Derrick
2020-09-07: Inference of Extended Finite State Machines
Authors: Michael Foster, Achim D. Brucker, Ramsay G. Taylor and John Derrick
2020-08-31: Practical Algebraic Calculus Checker
Authors: Mathias Fleury and Daniela Kaufmann
2020-08-31: Some classical results in inductive inference of recursive functions
Author: Frank J. Balbach
2020-08-26: Relational Disjoint-Set Forests
Author: Walter Guttmann
2020-08-25: Extensions to the Comprehensive Framework for Saturation Theorem Proving
Authors: Jasmin Blanchette and Sophie Tourret
2020-08-25: Putting the `K' into Bird's derivation of Knuth-Morris-Pratt string matching
Author: Peter Gammie
2020-08-04: Amicable Numbers
Author: Angeliki Koutsoukou-Argyraki
2020-08-03: Ordinal Partitions
Author: Lawrence C. Paulson
2020-07-21: A Formal Proof of The Chandy--Lamport Distributed Snapshot Algorithm
Authors: Ben Fiedler and Dmitriy Traytel
2020-07-13: Relational Characterisations of Paths
Authors: Walter Guttmann and Peter Höfner
2020-06-01: A Formally Verified Checker of the Safe Distance Traffic Rules for Autonomous Vehicles
Authors: Albert Rizaldi and Fabian Immler
2020-05-23: A verified algorithm for computing the Smith normal form of a matrix
Author: Jose Divasón
2020-05-16: The Nash-Williams Partition Theorem
Author: Lawrence C. Paulson
2020-05-13: A Formalization of Knuth–Bendix Orders
Authors: Christian Sternagel and René Thiemann
2020-05-12: Irrationality Criteria for Series by Erdős and Straus
Authors: Angeliki Koutsoukou-Argyraki and Wenda Li
2020-05-11: Recursion Theorem in ZF
Author: Georgy Dunaev
2020-05-08: An Efficient Normalisation Procedure for Linear Temporal Logic: Isabelle/HOL Formalisation
Author: Salomon Sickert
2020-05-06: Formalization of Forcing in Isabelle/ZF
Authors: Emmanuel Gunther, Miguel Pagano and Pedro Sánchez Terraf
2020-05-02: Banach-Steinhaus Theorem
Authors: Dominique Unruh and Jose Manuel Rodriguez Caballero
2020-04-27: Attack Trees in Isabelle for GDPR compliance of IoT healthcare systems
Author: Florian Kammueller
2020-04-24: Power Sum Polynomials
Author: Manuel Eberl
2020-04-24: The Lambert W Function on the Reals
Author: Manuel Eberl
2020-04-24: Gaussian Integers
Author: Manuel Eberl
2020-04-19: Matrices for ODEs
Author: Jonathan Julian Huerta y Munive
2020-04-16: Authenticated Data Structures As Functors
Authors: Andreas Lochbihler and Ognjen Marić
2020-04-10: Formalization of an Algorithm for Greedily Computing Associative Aggregations on Sliding Windows
Authors: Lukas Heimes, Dmitriy Traytel and Joshua Schneider
2020-04-09: A Comprehensive Framework for Saturation Theorem Proving
Author: Sophie Tourret
2020-04-09: Formalization of an Optimized Monitoring Algorithm for Metric First-Order Dynamic Logic with Aggregations
Authors: Thibault Dardinier, Lukas Heimes, Martin Raszyk, Joshua Schneider and Dmitriy Traytel
2020-04-08: Stateful Protocol Composition and Typing
Authors: Andreas V. Hess, Sebastian Mödersheim and Achim D. Brucker
2020-04-08: Automated Stateful Protocol Verification
Authors: Andreas V. Hess, Sebastian Mödersheim, Achim D. Brucker and Anders Schlichtkrull
2020-04-07: Lucas's Theorem
Author: Chelsea Edmonds
2020-03-25: Strong Eventual Consistency of the Collaborative Editing Framework WOOT
Authors: Emin Karayel and Edgar Gonzàlez
2020-03-22: Furstenberg's topology and his proof of the infinitude of primes
Author: Manuel Eberl
2020-03-12: An Under-Approximate Relational Logic
Author: Toby Murray
2020-03-07: Hello World
Authors: Cornelius Diekmann and Lars Hupel
2020-02-21: Implementing the Goodstein Function in λ-Calculus
Author: Bertram Felgenhauer
2020-02-10: A Generic Framework for Verified Compilers
Author: Martin Desharnais
2020-02-01: Arithmetic progressions and relative primes
Author: José Manuel Rodríguez Caballero
2020-01-31: A Hierarchy of Algebras for Boolean Subsets
Authors: Walter Guttmann and Bernhard Möller
2020-01-17: Mersenne primes and the Lucas–Lehmer test
Author: Manuel Eberl
2020-01-16: Verified Approximation Algorithms
Authors: Robin Eßmann, Tobias Nipkow and Simon Robillard
2020-01-13: Closest Pair of Points Algorithms
Authors: Martin Rau and Tobias Nipkow
2020-01-09: Skip Lists
Authors: Max W. Haslbeck and Manuel Eberl
2020-01-06: Bicategories
Author: Eugene W. Stark

 

2019
2019-12-27: The Irrationality of ζ(3)
Author: Manuel Eberl
2019-12-20: Formalizing a Seligman-Style Tableau System for Hybrid Logic
Author: Asta Halkjær From
2019-12-18: The Poincaré-Bendixson Theorem
Authors: Fabian Immler and Yong Kiam Tan
2019-12-16: Poincaré Disc Model
Authors: Danijela Simić, Filip Marić and Pierre Boutry
2019-12-16: Complex Geometry
Authors: Filip Marić and Danijela Simić
2019-12-10: Gauss Sums and the Pólya–Vinogradov Inequality
Authors: Rodrigo Raya and Manuel Eberl
2019-12-04: An Efficient Generalization of Counting Sort for Large, possibly Infinite Key Ranges
Author: Pasquale Noce
2019-11-27: Interval Arithmetic on 32-bit Words
Author: Brandon Bohrer
2019-10-24: Zermelo Fraenkel Set Theory in Higher-Order Logic
Author: Lawrence C. Paulson
2019-10-22: Isabelle/C
Authors: Frédéric Tuong and Burkhart Wolff
2019-10-16: VerifyThis 2019 -- Polished Isabelle Solutions
Authors: Peter Lammich and Simon Wimmer
2019-10-08: Aristotle's Assertoric Syllogistic
Author: Angeliki Koutsoukou-Argyraki
2019-10-07: Sigma Protocols and Commitment Schemes
Authors: David Butler and Andreas Lochbihler
2019-10-04: Clean - An Abstract Imperative Programming Language and its Theory
Authors: Frédéric Tuong and Burkhart Wolff
2019-09-16: Formalization of Multiway-Join Algorithms
Author: Thibault Dardinier
2019-09-10: Verification Components for Hybrid Systems
Author: Jonathan Julian Huerta y Munive
2019-09-06: Fourier Series
Author: Lawrence C Paulson
2019-08-30: A Case Study in Basic Algebra
Author: Clemens Ballarin
2019-08-16: Formalisation of an Adaptive State Counting Algorithm
Author: Robert Sachtleben
2019-08-14: Laplace Transform
Author: Fabian Immler
2019-08-06: Linear Programming
Authors: Julian Parsert and Cezary Kaliszyk
2019-08-06: Communicating Concurrent Kleene Algebra for Distributed Systems Specification
Authors: Maxime Buyse and Jason Jaskolka
2019-08-05: Selected Problems from the International Mathematical Olympiad 2019
Author: Manuel Eberl
2019-08-01: Stellar Quorum Systems
Author: Giuliano Losa
2019-07-30: A Formal Development of a Polychronous Polytimed Coordination Language
Authors: Hai Nguyen Van, Frédéric Boulanger and Burkhart Wolff
2019-07-27: Szpilrajn Extension Theorem
Author: Peter Zeller
2019-07-18: A Sequent Calculus for First-Order Logic
Author: Asta Halkjær From
2019-07-08: A Verified Code Generator from Isabelle/HOL to CakeML
Author: Lars Hupel
2019-07-04: Formalization of a Monitoring Algorithm for Metric First-Order Temporal Logic
Authors: Joshua Schneider and Dmitriy Traytel
2019-06-27: Complete Non-Orders and Fixed Points
Authors: Akihisa Yamada and Jérémy Dubut
2019-06-25: Priority Search Trees
Authors: Peter Lammich and Tobias Nipkow
2019-06-25: Purely Functional, Simple, and Efficient Implementation of Prim and Dijkstra
Authors: Peter Lammich and Tobias Nipkow
2019-06-21: Linear Inequalities
Authors: - Ralph Bottesch, + Ralph Bottesch, Alban Reynaud and René Thiemann
2019-06-16: Hilbert's Nullstellensatz
Author: Alexander Maletzky
2019-06-15: Gröbner Bases, Macaulay Matrices and Dubé's Degree Bounds
Author: Alexander Maletzky
2019-06-13: Binary Heaps for IMP2
Author: Simon Griebel
2019-06-03: Differential Game Logic
Author: André Platzer
2019-05-30: Multidimensional Binary Search Trees
Author: Martin Rau
2019-05-14: Formalization of Generic Authenticated Data Structures
Authors: Matthias Brun and Dmitriy Traytel
2019-05-09: Multi-Party Computation
Authors: David Aspinall and David Butler
2019-04-26: HOL-CSP Version 2.0
Authors: Safouan Taha, Lina Ye and Burkhart Wolff
2019-04-16: A Compositional and Unified Translation of LTL into ω-Automata
Authors: Benedikt Seidl and Salomon Sickert
2019-04-06: A General Theory of Syntax with Bindings
Authors: Lorenzo Gheri and Andrei Popescu
2019-03-27: The Transcendence of Certain Infinite Series
Authors: Angeliki Koutsoukou-Argyraki and Wenda Li
2019-03-24: Quantum Hoare Logic
Authors: Junyi Liu, Bohua Zhan, Shuling Wang, Shenggang Ying, Tao Liu, Yangjia Li, Mingsheng Ying and Naijun Zhan
2019-03-09: Safe OCL
Author: Denis Nikiforov
2019-02-21: Elementary Facts About the Distribution of Primes
Author: Manuel Eberl
2019-02-14: Kruskal's Algorithm for Minimum Spanning Forest
Authors: Maximilian P.L. Haslbeck, Peter Lammich and Julian Biendarra
2019-02-11: Probabilistic Primality Testing
Authors: Daniel Stüwe and Manuel Eberl
2019-02-08: Universal Turing Machine
Authors: Jian Xu, Xingyuan Zhang, Christian Urban and Sebastiaan J. C. Joosten
2019-02-01: Isabelle/UTP: Mechanised Theory Engineering for Unifying Theories of Programming
Authors: Simon Foster, Frank Zeyda, Yakoub Nemouchi, Pedro Ribeiro and Burkhart Wolff
2019-02-01: The Inversions of a List
Author: Manuel Eberl
2019-01-17: Farkas' Lemma and Motzkin's Transposition Theorem
Authors: - Ralph Bottesch, + Ralph Bottesch, Max W. Haslbeck and René Thiemann
2019-01-15: IMP2 – Simple Program Verification in Isabelle/HOL
Authors: Peter Lammich and Simon Wimmer
2019-01-15: An Algebra for Higher-Order Terms
Author: Lars Hupel
2019-01-07: A Reduction Theorem for Store Buffers
Authors: Ernie Cohen and Norbert Schirmer

 

2018
2018-12-26: A Formal Model of the Document Object Model
Authors: Achim D. Brucker and Michael Herzberg
2018-12-25: Formalization of Concurrent Revisions
Author: Roy Overbeek
2018-12-21: Verifying Imperative Programs using Auto2
Author: Bohua Zhan
2018-12-17: Constructive Cryptography in HOL
Authors: Andreas Lochbihler and S. Reza Sefidgar
2018-12-11: Transformer Semantics
Author: Georg Struth
2018-12-11: Quantales
Author: Georg Struth
2018-12-11: Properties of Orderings and Lattices
Author: Georg Struth
2018-11-23: Graph Saturation
Author: Sebastiaan J. C. Joosten
2018-11-23: A Verified Functional Implementation of Bachmair and Ganzinger's Ordered Resolution Prover
Authors: Anders Schlichtkrull, Jasmin Christian Blanchette and Dmitriy Traytel
2018-11-20: Auto2 Prover
Author: Bohua Zhan
2018-11-16: Matroids
Author: Jonas Keinholz
2018-11-06: Deriving generic class instances for datatypes
Authors: Jonas Rädle and Lars Hupel
2018-10-30: Formalisation and Evaluation of Alan Gewirth's Proof for the Principle of Generic Consistency in Isabelle/HOL
Authors: David Fuenmayor and Christoph Benzmüller
2018-10-29: Epistemic Logic
Author: Asta Halkjær From
2018-10-22: Smooth Manifolds
Authors: Fabian Immler and Bohua Zhan
2018-10-19: Randomised Binary Search Trees
Author: Manuel Eberl
2018-10-19: Formalization of the Embedding Path Order for Lambda-Free Higher-Order Terms
Author: Alexander Bentkamp
2018-10-12: Upper Bounding Diameters of State Spaces of Factored Transition Systems
Authors: Friedrich Kurz and Mohammad Abdulaziz
2018-09-28: The Transcendence of π
Author: Manuel Eberl
2018-09-25: Symmetric Polynomials
Author: Manuel Eberl
2018-09-20: Signature-Based Gröbner Basis Algorithms
Author: Alexander Maletzky
2018-09-19: The Prime Number Theorem
Authors: Manuel Eberl and Lawrence C. Paulson
2018-09-15: Aggregation Algebras
Author: Walter Guttmann
2018-09-14: Octonions
Author: Angeliki Koutsoukou-Argyraki
2018-09-05: Quaternions
Author: Lawrence C. Paulson
2018-09-02: The Budan-Fourier Theorem and Counting Real Roots with Multiplicity
Author: Wenda Li
2018-08-24: An Incremental Simplex Algorithm with Unsatisfiable Core Generation
Authors: Filip Marić, Mirko Spasić and René Thiemann
2018-08-14: Minsky Machines
Author: Bertram Felgenhauer
2018-07-16: Pricing in discrete financial models
Author: Mnacho Echenim
2018-07-04: Von-Neumann-Morgenstern Utility Theorem
Authors: Julian Parsert and Cezary Kaliszyk
2018-06-23: Pell's Equation
Author: Manuel Eberl
2018-06-14: Projective Geometry
Author: Anthony Bordg
2018-06-14: The Localization of a Commutative Ring
Author: Anthony Bordg
2018-06-05: Partial Order Reduction
Author: Julian Brunner
2018-05-27: Optimal Binary Search Trees
Authors: Tobias Nipkow and Dániel Somogyi
2018-05-25: Hidden Markov Models
Author: Simon Wimmer
2018-05-24: Probabilistic Timed Automata
Authors: Simon Wimmer and Johannes Hölzl
2018-05-23: Irrational Rapidly Convergent Series
Authors: Angeliki Koutsoukou-Argyraki and Wenda Li
2018-05-23: Axiom Systems for Category Theory in Free Logic
Authors: Christoph Benzmüller and Dana Scott
2018-05-22: Monadification, Memoization and Dynamic Programming
Authors: Simon Wimmer, Shuwei Hu and Tobias Nipkow
2018-05-10: OpSets: Sequential Specifications for Replicated Datatypes
Authors: Martin Kleppmann, Victor B. F. Gomes, Dominic P. Mulligan and Alastair R. Beresford
2018-05-07: An Isabelle/HOL Formalization of the Modular Assembly Kit for Security Properties
Authors: Oliver Bračevac, Richard Gay, Sylvia Grewe, Heiko Mantel, Henning Sudbrock and Markus Tasch
2018-04-29: WebAssembly
Author: Conrad Watt
2018-04-27: VerifyThis 2018 - Polished Isabelle Solutions
Authors: Peter Lammich and Simon Wimmer
2018-04-24: Bounded Natural Functors with Covariance and Contravariance
Authors: Andreas Lochbihler and Joshua Schneider
2018-03-22: The Incompatibility of Fishburn-Strategyproofness and Pareto-Efficiency
Authors: Felix Brandt, Manuel Eberl, Christian Saile and Christian Stricker
2018-03-13: Weight-Balanced Trees
Authors: Tobias Nipkow and Stefan Dirix
2018-03-12: CakeML
Authors: Lars Hupel and Yu Zhang
2018-03-01: A Theory of Architectural Design Patterns
Author: Diego Marmsoler
2018-02-26: Hoare Logics for Time Bounds
Authors: Maximilian P. L. Haslbeck and Tobias Nipkow
2018-02-06: Treaps
Authors: Maximilian Haslbeck, Manuel Eberl and Tobias Nipkow
2018-02-06: A verified factorization algorithm for integer polynomials with polynomial complexity
Authors: Jose Divasón, Sebastiaan Joosten, René Thiemann and Akihisa Yamada
2018-02-06: First-Order Terms
Authors: Christian Sternagel and René Thiemann
2018-02-06: The Error Function
Author: Manuel Eberl
2018-02-02: A verified LLL algorithm
Authors: - Ralph Bottesch, + Ralph Bottesch, Jose Divasón, Maximilian Haslbeck, Sebastiaan Joosten, René Thiemann and Akihisa Yamada
2018-01-18: Formalization of Bachmair and Ganzinger's Ordered Resolution Prover
Authors: Anders Schlichtkrull, Jasmin Christian Blanchette, Dmitriy Traytel and Uwe Waldmann
2018-01-16: Gromov Hyperbolicity
Author: Sebastien Gouezel
2018-01-11: An Isabelle/HOL formalisation of Green's Theorem
Authors: Mohammad Abdulaziz and Lawrence C. Paulson
2018-01-08: Taylor Models
Authors: Christoph Traut and Fabian Immler

 

2017
2017-12-22: The Falling Factorial of a Sum
Author: Lukas Bulwahn
2017-12-21: The Median-of-Medians Selection Algorithm
Author: Manuel Eberl
2017-12-21: The Mason–Stothers Theorem
Author: Manuel Eberl
2017-12-21: Dirichlet L-Functions and Dirichlet's Theorem
Author: Manuel Eberl
2017-12-19: Operations on Bounded Natural Functors
Authors: Jasmin Christian Blanchette, Andrei Popescu and Dmitriy Traytel
2017-12-18: The string search algorithm by Knuth, Morris and Pratt
Authors: Fabian Hellauer and Peter Lammich
2017-11-22: Stochastic Matrices and the Perron-Frobenius Theorem
Author: René Thiemann
2017-11-09: The IMAP CmRDT
Authors: Tim Jungnickel, Lennart Oldenburg and Matthias Loibl
2017-11-06: Hybrid Multi-Lane Spatial Logic
Author: Sven Linker
2017-10-26: The Kuratowski Closure-Complement Theorem
Authors: Peter Gammie and Gianpaolo Gioiosa
2017-10-19: Transition Systems and Automata
Author: Julian Brunner
2017-10-19: Büchi Complementation
Author: Julian Brunner
2017-10-17: Evaluate Winding Numbers through Cauchy Indices
Author: Wenda Li
2017-10-17: Count the Number of Complex Roots
Author: Wenda Li
2017-10-14: Homogeneous Linear Diophantine Equations
Authors: Florian Messner, Julian Parsert, Jonas Schöpf and Christian Sternagel
2017-10-12: The Hurwitz and Riemann ζ Functions
Author: Manuel Eberl
2017-10-12: Linear Recurrences
Author: Manuel Eberl
2017-10-12: Dirichlet Series
Author: Manuel Eberl
2017-09-21: Computer-assisted Reconstruction and Assessment of E. J. Lowe's Modal Ontological Argument
Authors: David Fuenmayor and Christoph Benzmüller
2017-09-17: Representation and Partial Automation of the Principia Logico-Metaphysica in Isabelle/HOL
Author: Daniel Kirchner
2017-09-06: Anselm's God in Isabelle/HOL
Author: Ben Blumson
2017-09-01: Microeconomics and the First Welfare Theorem
Authors: Julian Parsert and Cezary Kaliszyk
2017-08-20: Root-Balanced Tree
Author: Tobias Nipkow
2017-08-20: Orbit-Stabiliser Theorem with Application to Rotational Symmetries
Author: Jonas Rädle
2017-08-16: The LambdaMu-calculus
Authors: Cristina Matache, Victor B. F. Gomes and Dominic P. Mulligan
2017-07-31: Stewart's Theorem and Apollonius' Theorem
Author: Lukas Bulwahn
2017-07-28: Dynamic Architectures
Author: Diego Marmsoler
2017-07-21: Declarative Semantics for Functional Languages
Author: Jeremy Siek
2017-07-15: HOLCF-Prelude
Authors: Joachim Breitner, Brian Huffman, Neil Mitchell and Christian Sternagel
2017-07-13: Minkowski's Theorem
Author: Manuel Eberl
2017-07-09: Verified Metatheory and Type Inference for a Name-Carrying Simply-Typed Lambda Calculus
Author: Michael Rawson
2017-07-07: A framework for establishing Strong Eventual Consistency for Conflict-free Replicated Datatypes
Authors: Victor B. F. Gomes, Martin Kleppmann, Dominic P. Mulligan and Alastair R. Beresford
2017-07-06: Stone-Kleene Relation Algebras
Author: Walter Guttmann
2017-06-21: Propositional Proof Systems
Authors: Julius Michaelis and Tobias Nipkow
2017-06-13: Partial Semigroups and Convolution Algebras
Authors: Brijesh Dongol, Victor B. F. Gomes, Ian J. Hayes and Georg Struth
2017-06-06: Buffon's Needle Problem
Author: Manuel Eberl
2017-06-01: Formalizing Push-Relabel Algorithms
Authors: Peter Lammich and S. Reza Sefidgar
2017-06-01: Flow Networks and the Min-Cut-Max-Flow Theorem
Authors: Peter Lammich and S. Reza Sefidgar
2017-05-25: Optics
Authors: Simon Foster and Frank Zeyda
2017-05-24: Developing Security Protocols by Refinement
Authors: Christoph Sprenger and Ivano Somaini
2017-05-24: Dictionary Construction
Author: Lars Hupel
2017-05-08: The Floyd-Warshall Algorithm for Shortest Paths
Authors: Simon Wimmer and Peter Lammich
2017-05-05: Probabilistic while loop
Author: Andreas Lochbihler
2017-05-05: Effect polymorphism in higher-order logic
Author: Andreas Lochbihler
2017-05-05: Monad normalisation
Authors: Joshua Schneider, Manuel Eberl and Andreas Lochbihler
2017-05-05: Game-based cryptography in HOL
Authors: Andreas Lochbihler, S. Reza Sefidgar and Bhargav Bhatt
2017-05-05: CryptHOL
Author: Andreas Lochbihler
2017-05-04: Monoidal Categories
Author: Eugene W. Stark
2017-05-01: Types, Tableaus and Gödel’s God in Isabelle/HOL
Authors: David Fuenmayor and Christoph Benzmüller
2017-04-28: Local Lexing
Author: Steven Obua
2017-04-19: Constructor Functions
Author: Lars Hupel
2017-04-18: Lazifying case constants
Author: Lars Hupel
2017-04-06: Subresultants
Authors: Sebastiaan Joosten, René Thiemann and Akihisa Yamada
2017-04-04: Expected Shape of Random Binary Search Trees
Author: Manuel Eberl
2017-03-15: The number of comparisons in QuickSort
Author: Manuel Eberl
2017-03-15: Lower bound on comparison-based sorting algorithms
Author: Manuel Eberl
2017-03-10: The Euler–MacLaurin Formula
Author: Manuel Eberl
2017-02-28: The Group Law for Elliptic Curves
Author: Stefan Berghofer
2017-02-26: Menger's Theorem
Author: Christoph Dittmann
2017-02-13: Differential Dynamic Logic
Author: Brandon Bohrer
2017-02-10: Abstract Soundness
Authors: Jasmin Christian Blanchette, Andrei Popescu and Dmitriy Traytel
2017-02-07: Stone Relation Algebras
Author: Walter Guttmann
2017-01-31: Refining Authenticated Key Agreement with Strong Adversaries
Authors: Joseph Lallemand and Christoph Sprenger
2017-01-24: Bernoulli Numbers
Authors: Lukas Bulwahn and Manuel Eberl
2017-01-17: Minimal Static Single Assignment Form
Authors: Max Wagner and Denis Lohner
2017-01-17: Bertrand's postulate
Authors: Julian Biendarra and Manuel Eberl
2017-01-12: The Transcendence of e
Author: Manuel Eberl
2017-01-08: Formal Network Models and Their Application to Firewall Policies
Authors: Achim D. Brucker, Lukas Brügger and Burkhart Wolff
2017-01-03: Verification of a Diffie-Hellman Password-based Authentication Protocol by Extending the Inductive Method
Author: Pasquale Noce
2017-01-01: First-Order Logic According to Harrison
Authors: Alexander Birch Jensen, Anders Schlichtkrull and Jørgen Villadsen

 

2016
2016-12-30: Concurrent Refinement Algebra and Rely Quotients
Authors: Julian Fell, Ian J. Hayes and Andrius Velykis
2016-12-29: The Twelvefold Way
Author: Lukas Bulwahn
2016-12-20: Proof Strategy Language
Author: Yutaka Nagashima
2016-12-07: Paraconsistency
Authors: Anders Schlichtkrull and Jørgen Villadsen
2016-11-29: COMPLX: A Verification Framework for Concurrent Imperative Programs
Authors: Sidney Amani, June Andronick, Maksym Bortin, Corey Lewis, Christine Rizkallah and Joseph Tuong
2016-11-23: Abstract Interpretation of Annotated Commands
Author: Tobias Nipkow
2016-11-16: Separata: Isabelle tactics for Separation Algebra
Authors: Zhe Hou, David Sanan, Alwen Tiu, Rajeev Gore and Ranald Clouston
2016-11-12: Formalization of Nested Multisets, Hereditary Multisets, and Syntactic Ordinals
Authors: Jasmin Christian Blanchette, Mathias Fleury and Dmitriy Traytel
2016-11-12: Formalization of Knuth–Bendix Orders for Lambda-Free Higher-Order Terms
Authors: Heiko Becker, Jasmin Christian Blanchette, Uwe Waldmann and Daniel Wand
2016-11-10: Expressiveness of Deep Learning
Author: Alexander Bentkamp
2016-10-25: Modal Logics for Nominal Transition Systems
Authors: Tjark Weber, Lars-Henrik Eriksson, Joachim Parrow, Johannes Borgström and Ramunas Gutkovas
2016-10-24: Stable Matching
Author: Peter Gammie
2016-10-21: LOFT — Verified Migration of Linux Firewalls to SDN
Authors: Julius Michaelis and Cornelius Diekmann
2016-10-19: Source Coding Theorem
Authors: Quentin Hibon and Lawrence C. Paulson
2016-10-19: A formal model for the SPARCv8 ISA and a proof of non-interference for the LEON3 processor
Authors: Zhe Hou, David Sanan, Alwen Tiu and Yang Liu
2016-10-14: The Factorization Algorithm of Berlekamp and Zassenhaus
Authors: Jose Divasón, Sebastiaan Joosten, René Thiemann and Akihisa Yamada
2016-10-11: Intersecting Chords Theorem
Author: Lukas Bulwahn
2016-10-05: Lp spaces
Author: Sebastien Gouezel
2016-09-30: Fisher–Yates shuffle
Author: Manuel Eberl
2016-09-29: Allen's Interval Calculus
Author: Fadoua Ghourabi
2016-09-23: Formalization of Recursive Path Orders for Lambda-Free Higher-Order Terms
Authors: Jasmin Christian Blanchette, Uwe Waldmann and Daniel Wand
2016-09-09: Iptables Semantics
Authors: Cornelius Diekmann and Lars Hupel
2016-09-06: A Variant of the Superposition Calculus
Author: Nicolas Peltier
2016-09-06: Stone Algebras
Author: Walter Guttmann
2016-09-01: Stirling's formula
Author: Manuel Eberl
2016-08-31: Routing
Authors: Julius Michaelis and Cornelius Diekmann
2016-08-24: Simple Firewall
Authors: Cornelius Diekmann, Julius Michaelis and Maximilian Haslbeck
2016-08-18: Infeasible Paths Elimination by Symbolic Execution Techniques: Proof of Correctness and Preservation of Paths
Authors: Romain Aissat, Frederic Voisin and Burkhart Wolff
2016-08-12: Formalizing the Edmonds-Karp Algorithm
Authors: Peter Lammich and S. Reza Sefidgar
2016-08-08: The Imperative Refinement Framework
Author: Peter Lammich
2016-08-07: Ptolemy's Theorem
Author: Lukas Bulwahn
2016-07-17: Surprise Paradox
Author: Joachim Breitner
2016-07-14: Pairing Heap
Authors: Hauke Brinkop and Tobias Nipkow
2016-07-05: A Framework for Verifying Depth-First Search Algorithms
Authors: Peter Lammich and René Neumann
2016-07-01: Chamber Complexes, Coxeter Systems, and Buildings
Author: Jeremy Sylvestre
2016-06-30: The Z Property
Authors: Bertram Felgenhauer, Julian Nagele, Vincent van Oostrom and Christian Sternagel
2016-06-30: The Resolution Calculus for First-Order Logic
Author: Anders Schlichtkrull
2016-06-28: IP Addresses
Authors: Cornelius Diekmann, Julius Michaelis and Lars Hupel
2016-06-28: Compositional Security-Preserving Refinement for Concurrent Imperative Programs
Authors: Toby Murray, Robert Sison, Edward Pierzchalski and Christine Rizkallah
2016-06-26: Category Theory with Adjunctions and Limits
Author: Eugene W. Stark
2016-06-26: Cardinality of Multisets
Author: Lukas Bulwahn
2016-06-25: A Dependent Security Type System for Concurrent Imperative Programs
Authors: Toby Murray, Robert Sison, Edward Pierzchalski and Christine Rizkallah
2016-06-21: Catalan Numbers
Author: Manuel Eberl
2016-06-18: Program Construction and Verification Components Based on Kleene Algebra
Authors: Victor B. F. Gomes and Georg Struth
2016-06-13: Conservation of CSP Noninterference Security under Concurrent Composition
Author: Pasquale Noce
2016-06-09: Finite Machine Word Library
Authors: Joel Beeren, Matthew Fernandez, Xin Gao, Gerwin Klein, Rafal Kolanski, Japheth Lim, Corey Lewis, Daniel Matichuk and Thomas Sewell
2016-05-31: Tree Decomposition
Author: Christoph Dittmann
2016-05-24: POSIX Lexing with Derivatives of Regular Expressions
Authors: Fahad Ausaf, Roy Dyckhoff and Christian Urban
2016-05-24: Cardinality of Equivalence Relations
Author: Lukas Bulwahn
2016-05-20: Perron-Frobenius Theorem for Spectral Radius Analysis
Authors: Jose Divasón, Ondřej Kunčar, René Thiemann and Akihisa Yamada
2016-05-20: The meta theory of the Incredible Proof Machine
Authors: Joachim Breitner and Denis Lohner
2016-05-18: A Constructive Proof for FLP
Authors: Benjamin Bisping, Paul-David Brodmann, Tim Jungnickel, Christina Rickmann, Henning Seidler, Anke Stüber, Arno Wilhelm-Weidner, Kirstin Peters and Uwe Nestmann
2016-05-09: A Formal Proof of the Max-Flow Min-Cut Theorem for Countable Networks
Author: Andreas Lochbihler
2016-05-05: Randomised Social Choice Theory
Author: Manuel Eberl
2016-05-04: The Incompatibility of SD-Efficiency and SD-Strategy-Proofness
Author: Manuel Eberl
2016-05-04: Spivey's Generalized Recurrence for Bell Numbers
Author: Lukas Bulwahn
2016-05-02: Gröbner Bases Theory
Authors: Fabian Immler and Alexander Maletzky
2016-04-28: No Faster-Than-Light Observers
Authors: Mike Stannett and István Németi
2016-04-27: Algorithms for Reduced Ordered Binary Decision Diagrams
Authors: Julius Michaelis, Maximilian Haslbeck, Peter Lammich and Lars Hupel
2016-04-27: A formalisation of the Cocke-Younger-Kasami algorithm
Author: Maksym Bortin
2016-04-26: Conservation of CSP Noninterference Security under Sequential Composition
Author: Pasquale Noce
2016-04-12: Kleene Algebras with Domain
Authors: Victor B. F. Gomes, Walter Guttmann, Peter Höfner, Georg Struth and Tjark Weber
2016-03-11: Propositional Resolution and Prime Implicates Generation
Author: Nicolas Peltier
2016-03-08: Timed Automata
Author: Simon Wimmer
2016-03-08: The Cartan Fixed Point Theorems
Author: Lawrence C. Paulson
2016-03-01: Linear Temporal Logic
Author: Salomon Sickert
2016-02-17: Analysis of List Update Algorithms
Authors: Maximilian P.L. Haslbeck and Tobias Nipkow
2016-02-05: Verified Construction of Static Single Assignment Form
Authors: Sebastian Ullrich and Denis Lohner
2016-01-29: Polynomial Interpolation
Authors: René Thiemann and Akihisa Yamada
2016-01-29: Polynomial Factorization
Authors: René Thiemann and Akihisa Yamada
2016-01-20: Knot Theory
Author: T.V.H. Prathamesh
2016-01-18: Tensor Product of Matrices
Author: T.V.H. Prathamesh
2016-01-14: Cardinality of Number Partitions
Author: Lukas Bulwahn

 

2015
2015-12-28: Basic Geometric Properties of Triangles
Author: Manuel Eberl
2015-12-28: The Divergence of the Prime Harmonic Series
Author: Manuel Eberl
2015-12-28: Liouville numbers
Author: Manuel Eberl
2015-12-28: Descartes' Rule of Signs
Author: Manuel Eberl
2015-12-22: The Stern-Brocot Tree
Authors: Peter Gammie and Andreas Lochbihler
2015-12-22: Applicative Lifting
Authors: Andreas Lochbihler and Joshua Schneider
2015-12-22: Algebraic Numbers in Isabelle/HOL
Authors: René Thiemann, Akihisa Yamada and Sebastiaan Joosten
2015-12-12: Cardinality of Set Partitions
Author: Lukas Bulwahn
2015-12-02: Latin Square
Author: Alexander Bentkamp
2015-12-01: Ergodic Theory
Author: Sebastien Gouezel
2015-11-19: Euler's Partition Theorem
Author: Lukas Bulwahn
2015-11-18: The Tortoise and Hare Algorithm
Author: Peter Gammie
2015-11-11: Planarity Certificates
Author: Lars Noschinski
2015-11-02: Positional Determinacy of Parity Games
Author: Christoph Dittmann
2015-09-16: A Meta-Model for the Isabelle API
Authors: Frédéric Tuong and Burkhart Wolff
2015-09-04: Converting Linear Temporal Logic to Deterministic (Generalized) Rabin Automata
Author: Salomon Sickert
2015-08-21: Matrices, Jordan Normal Forms, and Spectral Radius Theory
Authors: René Thiemann and Akihisa Yamada
2015-08-20: Decreasing Diagrams II
Author: Bertram Felgenhauer
2015-08-18: The Inductive Unwinding Theorem for CSP Noninterference Security
Author: Pasquale Noce
2015-08-12: Representations of Finite Groups
Author: Jeremy Sylvestre
2015-08-10: Analysing and Comparing Encodability Criteria for Process Calculi
Authors: Kirstin Peters and Rob van Glabbeek
2015-07-21: Generating Cases from Labeled Subgoals
Author: Lars Noschinski
2015-07-14: Landau Symbols
Author: Manuel Eberl
2015-07-14: The Akra-Bazzi theorem and the Master theorem
Author: Manuel Eberl
2015-07-07: Hermite Normal Form
Authors: Jose Divasón and Jesús Aransay
2015-06-27: Derangements Formula
Author: Lukas Bulwahn
2015-06-11: The Ipurge Unwinding Theorem for CSP Noninterference Security
Author: Pasquale Noce
2015-06-11: The Generic Unwinding Theorem for CSP Noninterference Security
Author: Pasquale Noce
2015-06-11: Binary Multirelations
Authors: Hitoshi Furusawa and Georg Struth
2015-06-11: Reasoning about Lists via List Interleaving
Author: Pasquale Noce
2015-06-07: Parameterized Dynamic Tables
Author: Tobias Nipkow
2015-05-28: Derivatives of Logical Formulas
Author: Dmitriy Traytel
2015-05-27: A Zoo of Probabilistic Systems
Authors: Johannes Hölzl, Andreas Lochbihler and Dmitriy Traytel
2015-04-30: VCG - Combinatorial Vickrey-Clarke-Groves Auctions
Authors: Marco B. Caminati, Manfred Kerber, Christoph Lange and Colin Rowat
2015-04-15: Residuated Lattices
Authors: Victor B. F. Gomes and Georg Struth
2015-04-13: Concurrent IMP
Author: Peter Gammie
2015-04-13: Relaxing Safely: Verified On-the-Fly Garbage Collection for x86-TSO
Authors: Peter Gammie, Tony Hosking and Kai Engelhardt
2015-03-30: Trie
Authors: Andreas Lochbihler and Tobias Nipkow
2015-03-18: Consensus Refined
Authors: Ognjen Maric and Christoph Sprenger
2015-03-11: Deriving class instances for datatypes
Authors: Christian Sternagel and René Thiemann
2015-02-20: The Safety of Call Arity
Author: Joachim Breitner
2015-02-12: QR Decomposition
Authors: Jose Divasón and Jesús Aransay
2015-02-12: Echelon Form
Authors: Jose Divasón and Jesús Aransay
2015-02-05: Finite Automata in Hereditarily Finite Set Theory
Author: Lawrence C. Paulson
2015-01-28: Verification of the UpDown Scheme
Author: Johannes Hölzl

 

2014
2014-11-28: The Unified Policy Framework (UPF)
Authors: Achim D. Brucker, Lukas Brügger and Burkhart Wolff
2014-10-23: Loop freedom of the (untimed) AODV routing protocol
Authors: Timothy Bourke and Peter Höfner
2014-10-13: Lifting Definition Option
Author: René Thiemann
2014-10-10: Stream Fusion in HOL with Code Generation
Authors: Andreas Lochbihler and Alexandra Maximova
2014-10-09: A Verified Compiler for Probability Density Functions
Authors: Manuel Eberl, Johannes Hölzl and Tobias Nipkow
2014-10-08: Formalization of Refinement Calculus for Reactive Systems
Author: Viorel Preoteasa
2014-10-03: XML
Authors: Christian Sternagel and René Thiemann
2014-10-03: Certification Monads
Authors: Christian Sternagel and René Thiemann
2014-09-25: Imperative Insertion Sort
Author: Christian Sternagel
2014-09-19: The Sturm-Tarski Theorem
Author: Wenda Li
2014-09-15: The Cayley-Hamilton Theorem
Authors: Stephan Adelsberger, Stefan Hetzl and Florian Pollak
2014-09-09: The Jordan-Hölder Theorem
Author: Jakob von Raumer
2014-09-04: Priority Queues Based on Braun Trees
Author: Tobias Nipkow
2014-09-03: Gauss-Jordan Algorithm and Its Applications
Authors: Jose Divasón and Jesús Aransay
2014-08-29: Vector Spaces
Author: Holden Lee
2014-08-29: Real-Valued Special Functions: Upper and Lower Bounds
Author: Lawrence C. Paulson
2014-08-13: Skew Heap
Author: Tobias Nipkow
2014-08-12: Splay Tree
Author: Tobias Nipkow
2014-07-29: Haskell's Show Class in Isabelle/HOL
Authors: Christian Sternagel and René Thiemann
2014-07-18: Formal Specification of a Generic Separation Kernel
Authors: Freek Verbeek, Sergey Tverdyshev, Oto Havle, Holger Blasum, Bruno Langenstein, Werner Stephan, Yakoub Nemouchi, Abderrahmane Feliachi, Burkhart Wolff and Julien Schmaltz
2014-07-13: pGCL for Isabelle
Author: David Cock
2014-07-07: Amortized Complexity Verified
Author: Tobias Nipkow
2014-07-04: Network Security Policy Verification
Author: Cornelius Diekmann
2014-07-03: Pop-Refinement
Author: Alessandro Coglio
2014-06-12: Decision Procedures for MSO on Words Based on Derivatives of Regular Expressions
Authors: Dmitriy Traytel and Tobias Nipkow
2014-06-08: Boolean Expression Checkers
Author: Tobias Nipkow
2014-05-28: Promela Formalization
Author: René Neumann
2014-05-28: Converting Linear-Time Temporal Logic to Generalized Büchi Automata
Authors: Alexander Schimpf and Peter Lammich
2014-05-28: Verified Efficient Implementation of Gabow's Strongly Connected Components Algorithm
Author: Peter Lammich
2014-05-28: A Fully Verified Executable LTL Model Checker
Authors: Javier Esparza, Peter Lammich, René Neumann, Tobias Nipkow, Alexander Schimpf and Jan-Georg Smaus
2014-05-28: The CAVA Automata Library
Author: Peter Lammich
2014-05-23: Transitive closure according to Roy-Floyd-Warshall
Author: Makarius Wenzel
2014-05-23: Noninterference Security in Communicating Sequential Processes
Author: Pasquale Noce
2014-05-21: Regular Algebras
Authors: Simon Foster and Georg Struth
2014-04-28: Formalisation and Analysis of Component Dependencies
Author: Maria Spichkova
2014-04-23: A Formalization of Declassification with WHAT-and-WHERE-Security
Authors: Sylvia Grewe, Alexander Lux, Heiko Mantel and Jens Sauer
2014-04-23: A Formalization of Strong Security
Authors: Sylvia Grewe, Alexander Lux, Heiko Mantel and Jens Sauer
2014-04-23: A Formalization of Assumptions and Guarantees for Compositional Noninterference
Authors: Sylvia Grewe, Heiko Mantel and Daniel Schoepe
2014-04-22: Bounded-Deducibility Security
Authors: Andrei Popescu and Peter Lammich
2014-04-16: A shallow embedding of HyperCTL*
Authors: Markus N. Rabe, Peter Lammich and Andrei Popescu
2014-04-16: Abstract Completeness
Authors: Jasmin Christian Blanchette, Andrei Popescu and Dmitriy Traytel
2014-04-13: Discrete Summation
Author: Florian Haftmann
2014-04-03: Syntax and semantics of a GPU kernel programming language
Author: John Wickerson
2014-03-11: Probabilistic Noninterference
Authors: Andrei Popescu and Johannes Hölzl
2014-03-08: Mechanization of the Algebra for Wireless Networks (AWN)
Author: Timothy Bourke
2014-02-18: Mutually Recursive Partial Functions
Author: René Thiemann
2014-02-13: Properties of Random Graphs -- Subgraph Containment
Author: Lars Hupel
2014-02-11: Verification of Selection and Heap Sort Using Locales
Author: Danijela Petrovic
2014-02-07: Affine Arithmetic
Author: Fabian Immler
2014-02-06: Implementing field extensions of the form Q[sqrt(b)]
Author: René Thiemann
2014-01-30: Unified Decision Procedures for Regular Expression Equivalence
Authors: Tobias Nipkow and Dmitriy Traytel
2014-01-28: Secondary Sylow Theorems
Author: Jakob von Raumer
2014-01-25: Relation Algebra
Authors: Alasdair Armstrong, Simon Foster, Georg Struth and Tjark Weber
2014-01-23: Kleene Algebra with Tests and Demonic Refinement Algebras
Authors: Alasdair Armstrong, Victor B. F. Gomes and Georg Struth
2014-01-16: Featherweight OCL: A Proposal for a Machine-Checked Formal Semantics for OCL 2.5
Authors: Achim D. Brucker, Frédéric Tuong and Burkhart Wolff
2014-01-11: Sturm's Theorem
Author: Manuel Eberl
2014-01-11: Compositional Properties of Crypto-Based Components
Author: Maria Spichkova

 

2013
2013-12-01: A General Method for the Proof of Theorems on Tail-recursive Functions
Author: Pasquale Noce
2013-11-17: Gödel's Incompleteness Theorems
Author: Lawrence C. Paulson
2013-11-17: The Hereditarily Finite Sets
Author: Lawrence C. Paulson
2013-11-15: A Codatatype of Formal Languages
Author: Dmitriy Traytel
2013-11-14: Stream Processing Components: Isabelle/HOL Formalisation and Case Studies
Author: Maria Spichkova
2013-11-12: Gödel's God in Isabelle/HOL
Authors: Christoph Benzmüller and Bruno Woltzenlogel Paleo
2013-11-01: Decreasing Diagrams
Author: Harald Zankl
2013-10-02: Automatic Data Refinement
Author: Peter Lammich
2013-09-17: Native Word
Author: Andreas Lochbihler
2013-07-27: A Formal Model of IEEE Floating Point Arithmetic
Author: Lei Yu
2013-07-22: Pratt's Primality Certificates
Authors: Simon Wimmer and Lars Noschinski
2013-07-22: Lehmer's Theorem
Authors: Simon Wimmer and Lars Noschinski
2013-07-19: The Königsberg Bridge Problem and the Friendship Theorem
Author: Wenda Li
2013-06-27: Sound and Complete Sort Encodings for First-Order Logic
Authors: Jasmin Christian Blanchette and Andrei Popescu
2013-05-22: An Axiomatic Characterization of the Single-Source Shortest Path Problem
Author: Christine Rizkallah
2013-04-28: Graph Theory
Author: Lars Noschinski
2013-04-15: Light-weight Containers
Author: Andreas Lochbihler
2013-02-21: Nominal 2
Authors: Christian Urban, Stefan Berghofer and Cezary Kaliszyk
2013-01-31: The Correctness of Launchbury's Natural Semantics for Lazy Evaluation
Author: Joachim Breitner
2013-01-19: Ribbon Proofs
Author: John Wickerson
2013-01-16: Rank-Nullity Theorem in Linear Algebra
Authors: Jose Divasón and Jesús Aransay
2013-01-15: Kleene Algebra
Authors: Alasdair Armstrong, Georg Struth and Tjark Weber
2013-01-03: Computing N-th Roots using the Babylonian Method
Author: René Thiemann

 

2012
2012-11-14: A Separation Logic Framework for Imperative HOL
Authors: Peter Lammich and Rene Meis
2012-11-02: Open Induction
Authors: Mizuhito Ogawa and Christian Sternagel
2012-10-30: The independence of Tarski's Euclidean axiom
Author: T. J. M. Makarios
2012-10-27: Bondy's Theorem
Authors: Jeremy Avigad and Stefan Hetzl
2012-09-10: Possibilistic Noninterference
Authors: Andrei Popescu and Johannes Hölzl
2012-08-07: Generating linear orders for datatypes
Author: René Thiemann
2012-08-05: Proving the Impossibility of Trisecting an Angle and Doubling the Cube
Authors: Ralph Romanos and Lawrence C. Paulson
2012-07-27: Verifying Fault-Tolerant Distributed Algorithms in the Heard-Of Model
Authors: Henri Debrat and Stephan Merz
2012-07-01: Logical Relations for PCF
Author: Peter Gammie
2012-06-26: Type Constructor Classes and Monad Transformers
Author: Brian Huffman
2012-05-29: Psi-calculi in Isabelle
Author: Jesper Bengtson
2012-05-29: The pi-calculus in nominal logic
Author: Jesper Bengtson
2012-05-29: CCS in nominal logic
Author: Jesper Bengtson
2012-05-27: Isabelle/Circus
Authors: Abderrahmane Feliachi, Burkhart Wolff and Marie-Claude Gaudel
2012-05-11: Separation Algebra
Authors: Gerwin Klein, Rafal Kolanski and Andrew Boyton
2012-05-07: Stuttering Equivalence
Author: Stephan Merz
2012-05-02: Inductive Study of Confidentiality
Author: Giampaolo Bella
2012-04-26: Ordinary Differential Equations
Authors: Fabian Immler and Johannes Hölzl
2012-04-13: Well-Quasi-Orders
Author: Christian Sternagel
2012-03-01: Abortable Linearizable Modules
Authors: Rachid Guerraoui, Viktor Kuncak and Giuliano Losa
2012-02-29: Executable Transitive Closures
Author: René Thiemann
2012-02-06: A Probabilistic Proof of the Girth-Chromatic Number Theorem
Author: Lars Noschinski
2012-01-30: Refinement for Monadic Programs
Author: Peter Lammich
2012-01-30: Dijkstra's Shortest Path Algorithm
Authors: Benedikt Nordhoff and Peter Lammich
2012-01-03: Markov Models
Authors: Johannes Hölzl and Tobias Nipkow

 

2011
2011-11-19: A Definitional Encoding of TLA* in Isabelle/HOL
Authors: Gudmund Grov and Stephan Merz
2011-11-09: Efficient Mergesort
Author: Christian Sternagel
2011-09-22: Pseudo Hoops
Authors: George Georgescu, Laurentiu Leustean and Viorel Preoteasa
2011-09-22: Algebra of Monotonic Boolean Transformers
Author: Viorel Preoteasa
2011-09-22: Lattice Properties
Author: Viorel Preoteasa
2011-08-26: The Myhill-Nerode Theorem Based on Regular Expressions
Authors: Chunhan Wu, Xingyuan Zhang and Christian Urban
2011-08-19: Gauss-Jordan Elimination for Matrices Represented as Functions
Author: Tobias Nipkow
2011-07-21: Maximum Cardinality Matching
Author: Christine Rizkallah
2011-05-17: Knowledge-based programs
Author: Peter Gammie
2011-04-01: The General Triangle Is Unique
Author: Joachim Breitner
2011-03-14: Executable Transitive Closures of Finite Relations
Authors: Christian Sternagel and René Thiemann
2011-02-23: Interval Temporal Logic on Natural Numbers
Author: David Trachtenherz
2011-02-23: Infinite Lists
Author: David Trachtenherz
2011-02-23: AutoFocus Stream Processing for Single-Clocking and Multi-Clocking Semantics
Author: David Trachtenherz
2011-02-07: Lightweight Java
Authors: Rok Strniša and Matthew Parkinson
2011-01-10: RIPEMD-160
Author: Fabian Immler
2011-01-08: Lower Semicontinuous Functions
Author: Bogdan Grechuk

 

2010
2010-12-17: Hall's Marriage Theorem
Authors: Dongchen Jiang and Tobias Nipkow
2010-11-16: Shivers' Control Flow Analysis
Author: Joachim Breitner
2010-10-28: Finger Trees
Authors: Benedikt Nordhoff, Stefan Körner and Peter Lammich
2010-10-28: Functional Binomial Queues
Author: René Neumann
2010-10-28: Binomial Heaps and Skew Binomial Heaps
Authors: Rene Meis, Finn Nielsen and Peter Lammich
2010-08-29: Strong Normalization of Moggis's Computational Metalanguage
Author: Christian Doczkal
2010-08-10: Executable Multivariate Polynomials
Authors: Christian Sternagel, René Thiemann, Alexander Maletzky, Fabian Immler, Florian Haftmann, Andreas Lochbihler and Alexander Bentkamp
2010-08-08: Formalizing Statecharts using Hierarchical Automata
Authors: Steffen Helke and Florian Kammüller
2010-06-24: Free Groups
Author: Joachim Breitner
2010-06-20: Category Theory
Author: Alexander Katovsky
2010-06-17: Executable Matrix Operations on Matrices of Arbitrary Dimensions
Authors: Christian Sternagel and René Thiemann
2010-06-14: Abstract Rewriting
Authors: Christian Sternagel and René Thiemann
2010-05-28: Verification of the Deutsch-Schorr-Waite Graph Marking Algorithm using Data Refinement
Authors: Viorel Preoteasa and Ralph-Johan Back
2010-05-28: Semantics and Data Refinement of Invariant Based Programs
Authors: Viorel Preoteasa and Ralph-Johan Back
2010-05-22: A Complete Proof of the Robbins Conjecture
Author: Matthew Wampler-Doty
2010-05-12: Regular Sets and Expressions
Authors: Alexander Krauss and Tobias Nipkow
2010-04-30: Locally Nameless Sigma Calculus
Authors: Ludovic Henrio, Florian Kammüller, Bianca Lutz and Henry Sudhof
2010-03-29: Free Boolean Algebra
Author: Brian Huffman
2010-03-23: Inter-Procedural Information Flow Noninterference via Slicing
Author: Daniel Wasserrab
2010-03-23: Information Flow Noninterference via Slicing
Author: Daniel Wasserrab
2010-02-20: List Index
Author: Tobias Nipkow
2010-02-12: Coinductive
Author: Andreas Lochbihler

 

2009
2009-12-09: A Fast SAT Solver for Isabelle in Standard ML
Author: Armin Heller
2009-12-03: Formalizing the Logic-Automaton Connection
Authors: Stefan Berghofer and Markus Reiter
2009-11-25: Tree Automata
Author: Peter Lammich
2009-11-25: Collections Framework
Author: Peter Lammich
2009-11-22: Perfect Number Theorem
Author: Mark Ijbema
2009-11-13: Backing up Slicing: Verifying the Interprocedural Two-Phase Horwitz-Reps-Binkley Slicer
Author: Daniel Wasserrab
2009-10-30: The Worker/Wrapper Transformation
Author: Peter Gammie
2009-09-01: Ordinals and Cardinals
Author: Andrei Popescu
2009-08-28: Invertibility in Sequent Calculi
Author: Peter Chapman
2009-08-04: An Example of a Cofinitary Group in Isabelle/HOL
Author: Bart Kastermans
2009-05-06: Code Generation for Functions as Data
Author: Andreas Lochbihler
2009-04-29: Stream Fusion
Author: Brian Huffman

 

2008
2008-12-12: A Bytecode Logic for JML and Types
Authors: Lennart Beringer and Martin Hofmann
2008-11-10: Secure information flow and program logics
Authors: Lennart Beringer and Martin Hofmann
2008-11-09: Some classical results in Social Choice Theory
Author: Peter Gammie
2008-11-07: Fun With Tilings
Authors: Tobias Nipkow and Lawrence C. Paulson
2008-10-15: The Textbook Proof of Huffman's Algorithm
Author: Jasmin Christian Blanchette
2008-09-16: Towards Certified Slicing
Author: Daniel Wasserrab
2008-09-02: A Correctness Proof for the Volpano/Smith Security Typing System
Authors: Gregor Snelting and Daniel Wasserrab
2008-09-01: Arrow and Gibbard-Satterthwaite
Author: Tobias Nipkow
2008-08-26: Fun With Functions
Author: Tobias Nipkow
2008-07-23: Formal Verification of Modern SAT Solvers
Author: Filip Marić
2008-04-05: Recursion Theory I
Author: Michael Nedzelsky
2008-02-29: A Sequential Imperative Programming Language Syntax, Semantics, Hoare Logics and Verification Environment
Author: Norbert Schirmer
2008-02-29: BDD Normalisation
Authors: Veronika Ortner and Norbert Schirmer
2008-02-18: Normalization by Evaluation
Authors: Klaus Aehlig and Tobias Nipkow
2008-01-11: Quantifier Elimination for Linear Arithmetic
Author: Tobias Nipkow

 

2007
2007-12-14: Formalization of Conflict Analysis of Programs with Procedures, Thread Creation, and Monitors
Authors: Peter Lammich and Markus Müller-Olm
2007-12-03: Jinja with Threads
Author: Andreas Lochbihler
2007-11-06: Much Ado About Two
Author: Sascha Böhme
2007-08-12: Sums of Two and Four Squares
Author: Roelof Oosterhuis
2007-08-12: Fermat's Last Theorem for Exponents 3 and 4 and the Parametrisation of Pythagorean Triples
Author: Roelof Oosterhuis
2007-08-08: Fundamental Properties of Valuation Theory and Hensel's Lemma
Author: Hidetsune Kobayashi
2007-08-02: POPLmark Challenge Via de Bruijn Indices
Author: Stefan Berghofer
2007-08-02: First-Order Logic According to Fitting
Author: Stefan Berghofer

 

2006
2006-09-09: Hotel Key Card System
Author: Tobias Nipkow
2006-08-08: Abstract Hoare Logics
Author: Tobias Nipkow
2006-05-22: Flyspeck I: Tame Graphs
Authors: Gertrud Bauer and Tobias Nipkow
2006-05-15: CoreC++
Author: Daniel Wasserrab
2006-03-31: A Theory of Featherweight Java in Isabelle/HOL
Authors: J. Nathan Foster and Dimitrios Vytiniotis
2006-03-15: Instances of Schneider's generalized protocol of clock synchronization
Author: Damián Barsotti
2006-03-14: Cauchy's Mean Theorem and the Cauchy-Schwarz Inequality
Author: Benjamin Porter

 

2005
2005-11-11: Countable Ordinals
Author: Brian Huffman
2005-10-12: Fast Fourier Transform
Author: Clemens Ballarin
2005-06-24: Formalization of a Generalized Protocol for Clock Synchronization
Author: Alwen Tiu
2005-06-22: Proving the Correctness of Disk Paxos
Authors: Mauro Jaskelioff and Stephan Merz
2005-06-20: Jive Data and Store Model
Authors: Nicole Rauch and Norbert Schirmer
2005-06-01: Jinja is not Java
Authors: Gerwin Klein and Tobias Nipkow
2005-05-02: SHA1, RSA, PSS and more
Authors: Christina Lindenberg and Kai Wirt
2005-04-21: Category Theory to Yoneda's Lemma
Author: Greg O'Keefe

 

2004
2004-12-09: File Refinement
Authors: Karen Zee and Viktor Kuncak
2004-11-19: Integration theory and random variables
Author: Stefan Richter
2004-09-28: A Mechanically Verified, Efficient, Sound and Complete Theorem Prover For First Order Logic
Author: Tom Ridge
2004-09-20: Ramsey's theorem, infinitary version
Author: Tom Ridge
2004-09-20: Completeness theorem
Authors: James Margetson and Tom Ridge
2004-07-09: Compiling Exceptions Correctly
Author: Tobias Nipkow
2004-06-24: Depth First Search
Authors: Toshiaki Nishihara and Yasuhiko Minamide
2004-05-18: Groups, Rings and Modules
Authors: Hidetsune Kobayashi, L. Chen and H. Murao
2004-04-26: Topology
Author: Stefan Friedrich
2004-04-26: Lazy Lists II
Author: Stefan Friedrich
2004-04-05: Binary Search Trees
Author: Viktor Kuncak
2004-03-30: Functional Automata
Author: Tobias Nipkow
2004-03-19: Mini ML
Authors: Wolfgang Naraschewski and Tobias Nipkow
2004-03-19: AVL Trees
Authors: Tobias Nipkow and Cornelia Pusch
\ No newline at end of file diff --git a/web/rss.xml b/web/rss.xml --- a/web/rss.xml +++ b/web/rss.xml @@ -1,599 +1,594 @@ Archive of Formal Proofs https://www.isa-afp.org The Archive of Formal Proofs is a collection of proof libraries, examples, and larger scientific developments, mechanically checked in the theorem prover Isabelle. - 03 Mar 2021 00:00:00 +0000 + 12 Mar 2021 00:00:00 +0000 + + Two algorithms based on modular arithmetic: lattice basis reduction and Hermite normal form computation + https://www.isa-afp.org/entries/Modular_arithmetic_LLL_and_HNF_algorithms.html + https://www.isa-afp.org/entries/Modular_arithmetic_LLL_and_HNF_algorithms.html + Ralph Bottesch, Jose Divason, Rene Thiemann + 12 Mar 2021 00:00:00 +0000 + +We verify two algorithms for which modular arithmetic plays an +essential role: Storjohann's variant of the LLL lattice basis +reduction algorithm and Kopparty's algorithm for computing the +Hermite normal form of a matrix. To do this, we also formalize some +facts about the modulo operation with symmetric range. Our +implementations are based on the original papers, but are otherwise +efficient. For basis reduction we formalize two versions: one that +includes all of the optimizations/heuristics from Storjohann's +paper, and one excluding a heuristic that we observed to often +decrease efficiency. We also provide a fast, self-contained certifier +for basis reduction, based on the efficient Hermite normal form +algorithm. + Quantum projective measurements and the CHSH inequality https://www.isa-afp.org/entries/Projective_Measurements.html https://www.isa-afp.org/entries/Projective_Measurements.html Mnacho Echenim 03 Mar 2021 00:00:00 +0000 This work contains a formalization of quantum projective measurements, also known as von Neumann measurements, which are based on elements of spectral theory. We also formalized the CHSH inequality, an inequality involving expectations in a probability space that is violated by quantum measurements, thus proving that quantum mechanics cannot be modeled with an underlying local hidden-variable theory. The Hermite–Lindemann–Weierstraß Transcendence Theorem https://www.isa-afp.org/entries/Hermite_Lindemann.html https://www.isa-afp.org/entries/Hermite_Lindemann.html Manuel Eberl 03 Mar 2021 00:00:00 +0000 <p>This article provides a formalisation of the Hermite-Lindemann-Weierstraß Theorem (also known as simply Hermite-Lindemann or Lindemann-Weierstraß). This theorem is one of the crowning achievements of 19th century number theory.</p> <p>The theorem states that if $\alpha_1, \ldots, \alpha_n\in\mathbb{C}$ are algebraic numbers that are linearly independent over $\mathbb{Z}$, then $e^{\alpha_1},\ldots,e^{\alpha_n}$ are algebraically independent over $\mathbb{Q}$.</p> <p>Like the <a href="https://doi.org/10.1007/978-3-319-66107-0_5">previous formalisation in Coq by Bernard</a>, I proceeded by formalising <a href="https://doi.org/10.1017/CBO9780511565977">Baker's version of the theorem and proof</a> and then deriving the original one from that. Baker's version states that for any algebraic numbers $\beta_1, \ldots, \beta_n\in\mathbb{C}$ and distinct algebraic numbers $\alpha_i, \ldots, \alpha_n\in\mathbb{C}$, we have $\beta_1 e^{\alpha_1} + \ldots + \beta_n e^{\alpha_n} = 0$ if and only if all the $\beta_i$ are zero.</p> <p>This has a number of direct corollaries, e.g.:</p> <ul> <li>$e$ and $\pi$ are transcendental</li> <li>$e^z$, $\sin z$, $\tan z$, etc. are transcendental for algebraic $z\in\mathbb{C}\setminus\{0\}$</li> <li>$\ln z$ is transcendental for algebraic $z\in\mathbb{C}\setminus\{0, 1\}$</li> </ul> Mereology https://www.isa-afp.org/entries/Mereology.html https://www.isa-afp.org/entries/Mereology.html Ben Blumson 01 Mar 2021 00:00:00 +0000 We use Isabelle/HOL to verify elementary theorems and alternative axiomatizations of classical extensional mereology. The Sunflower Lemma of Erdős and Rado https://www.isa-afp.org/entries/Sunflowers.html https://www.isa-afp.org/entries/Sunflowers.html René Thiemann 25 Feb 2021 00:00:00 +0000 We formally define sunflowers and provide a formalization of the sunflower lemma of Erd&odblac;s and Rado: whenever a set of size-<i>k</i>-sets has a larger cardinality than <i>(r - 1)<sup>k</sup> &middot; k!</i>, then it contains a sunflower of cardinality <i>r</i>. A Verified Imperative Implementation of B-Trees https://www.isa-afp.org/entries/BTree.html https://www.isa-afp.org/entries/BTree.html Niels Mündler 24 Feb 2021 00:00:00 +0000 In this work, we use the interactive theorem prover Isabelle/HOL to verify an imperative implementation of the classical B-tree data structure invented by Bayer and McCreight [ACM 1970]. The implementation supports set membership and insertion queries with efficient binary search for intra-node navigation. This is accomplished by first specifying the structure abstractly in the functional modeling language HOL and proving functional correctness. Using manual refinement, we derive an imperative implementation in Imperative/HOL. We show the validity of this refinement using the separation logic utilities from the <a href="https://www.isa-afp.org/entries/Refine_Imperative_HOL.html"> Isabelle Refinement Framework </a> . The code can be exported to the programming languages SML and Scala. We examine the runtime of all operations indirectly by reproducing results of the logarithmic relationship between height and the number of nodes. The results are discussed in greater detail in the corresponding <a href="https://mediatum.ub.tum.de/1596550">Bachelor's Thesis</a>. Formal Puiseux Series https://www.isa-afp.org/entries/Formal_Puiseux_Series.html https://www.isa-afp.org/entries/Formal_Puiseux_Series.html Manuel Eberl 17 Feb 2021 00:00:00 +0000 <p>Formal Puiseux series are generalisations of formal power series and formal Laurent series that also allow for fractional exponents. They have the following general form: \[\sum_{i=N}^\infty a_{i/d} X^{i/d}\] where <em>N</em> is an integer and <em>d</em> is a positive integer.</p> <p>This entry defines these series including their basic algebraic properties. Furthermore, it proves the Newton–Puiseux Theorem, namely that the Puiseux series over an algebraically closed field of characteristic 0 are also algebraically closed.</p> The Laws of Large Numbers https://www.isa-afp.org/entries/Laws_of_Large_Numbers.html https://www.isa-afp.org/entries/Laws_of_Large_Numbers.html Manuel Eberl 10 Feb 2021 00:00:00 +0000 <p>The Law of Large Numbers states that, informally, if one performs a random experiment $X$ many times and takes the average of the results, that average will be very close to the expected value $E[X]$.</p> <p> More formally, let $(X_i)_{i\in\mathbb{N}}$ be a sequence of independently identically distributed random variables whose expected value $E[X_1]$ exists. Denote the running average of $X_1, \ldots, X_n$ as $\overline{X}_n$. Then:</p> <ul> <li>The Weak Law of Large Numbers states that $\overline{X}_{n} \longrightarrow E[X_1]$ in probability for $n\to\infty$, i.e. $\mathcal{P}(|\overline{X}_{n} - E[X_1]| > \varepsilon) \longrightarrow 0$ as $n\to\infty$ for any $\varepsilon > 0$.</li> <li>The Strong Law of Large Numbers states that $\overline{X}_{n} \longrightarrow E[X_1]$ almost surely for $n\to\infty$, i.e. $\mathcal{P}(\overline{X}_{n} \longrightarrow E[X_1]) = 1$.</li> </ul> <p>In this entry, I formally prove the strong law and from it the weak law. The approach used for the proof of the strong law is a particularly quick and slick one based on ergodic theory, which was formalised by Gouëzel in another AFP entry.</p> Tarski's Parallel Postulate implies the 5th Postulate of Euclid, the Postulate of Playfair and the original Parallel Postulate of Euclid https://www.isa-afp.org/entries/IsaGeoCoq.html https://www.isa-afp.org/entries/IsaGeoCoq.html Roland Coghetto 31 Jan 2021 00:00:00 +0000 <p>The <a href="https://geocoq.github.io/GeoCoq/">GeoCoq library</a> contains a formalization of geometry using the Coq proof assistant. It contains both proofs about the foundations of geometry and high-level proofs in the same style as in high school. We port a part of the GeoCoq 2.4.0 library to Isabelle/HOL: more precisely, the files Chap02.v to Chap13_3.v, suma.v as well as the associated definitions and some useful files for the demonstration of certain parallel postulates. The synthetic approach of the demonstrations is directly inspired by those contained in GeoCoq. The names of the lemmas and theorems used are kept as far as possible as well as the definitions. </p> <p>It should be noted that T.J.M. Makarios has done <a href="https://www.isa-afp.org/entries/Tarskis_Geometry.html">some proofs in Tarski's Geometry</a>. It uses a definition that does not quite coincide with the definition used in Geocoq and here. Furthermore, corresponding definitions in the <a href="https://www.isa-afp.org/entries/Poincare_Disc.html">Poincaré Disc Model development</a> are not identical to those defined in GeoCoq. </p> <p>In the last part, it is formalized that, in the neutral/absolute space, the axiom of the parallels of Tarski's system implies the Playfair axiom, the 5th postulate of Euclid and Euclid's original parallel postulate. These proofs, which are not constructive, are directly inspired by Pierre Boutry, Charly Gries, Julien Narboux and Pascal Schreck. </p> Solution to the xkcd Blue Eyes puzzle https://www.isa-afp.org/entries/Blue_Eyes.html https://www.isa-afp.org/entries/Blue_Eyes.html Jakub Kądziołka 30 Jan 2021 00:00:00 +0000 In a <a href="https://xkcd.com/blue_eyes.html">puzzle published by Randall Munroe</a>, perfect logicians forbidden from communicating are stranded on an island, and may only leave once they have figured out their own eye color. We present a method of modeling the behavior of perfect logicians and formalize a solution of the puzzle. Hood-Melville Queue https://www.isa-afp.org/entries/Hood_Melville_Queue.html https://www.isa-afp.org/entries/Hood_Melville_Queue.html Alejandro Gómez-Londoño 18 Jan 2021 00:00:00 +0000 This is a verified implementation of a constant time queue. The original design is due to <a href="https://doi.org/10.1016/0020-0190(81)90030-2">Hood and Melville</a>. This formalization follows the presentation in <em>Purely Functional Data Structures</em>by Okasaki. JinjaDCI: a Java semantics with dynamic class initialization https://www.isa-afp.org/entries/JinjaDCI.html https://www.isa-afp.org/entries/JinjaDCI.html Susannah Mansky 11 Jan 2021 00:00:00 +0000 We extend Jinja to include static fields, methods, and instructions, and dynamic class initialization, based on the Java SE 8 specification. This includes extension of definitions and proofs. This work is partially described in Mansky and Gunter's paper at CPP 2019 and Mansky's doctoral thesis (UIUC, 2020). Cofinality and the Delta System Lemma https://www.isa-afp.org/entries/Delta_System_Lemma.html https://www.isa-afp.org/entries/Delta_System_Lemma.html Pedro Sánchez Terraf 27 Dec 2020 00:00:00 +0000 We formalize the basic results on cofinality of linearly ordered sets and ordinals and Šanin’s Lemma for uncountable families of finite sets. This last result is used to prove the countable chain condition for Cohen posets. We work in the set theory framework of Isabelle/ZF, using the Axiom of Choice as needed. Topological semantics for paraconsistent and paracomplete logics https://www.isa-afp.org/entries/Topological_Semantics.html https://www.isa-afp.org/entries/Topological_Semantics.html David Fuenmayor 17 Dec 2020 00:00:00 +0000 We introduce a generalized topological semantics for paraconsistent and paracomplete logics by drawing upon early works on topological Boolean algebras (cf. works by Kuratowski, Zarycki, McKinsey & Tarski, etc.). In particular, this work exemplarily illustrates the shallow semantical embeddings approach (<a href="http://dx.doi.org/10.1007/s11787-012-0052-y">SSE</a>) employing the proof assistant Isabelle/HOL. By means of the SSE technique we can effectively harness theorem provers, model finders and 'hammers' for reasoning with quantified non-classical logics. Relational Minimum Spanning Tree Algorithms https://www.isa-afp.org/entries/Relational_Minimum_Spanning_Trees.html https://www.isa-afp.org/entries/Relational_Minimum_Spanning_Trees.html Walter Guttmann, Nicolas Robinson-O'Brien 08 Dec 2020 00:00:00 +0000 We verify the correctness of Prim's, Kruskal's and Borůvka's minimum spanning tree algorithms based on algebras for aggregation and minimisation. Inline Caching and Unboxing Optimization for Interpreters https://www.isa-afp.org/entries/Interpreter_Optimizations.html https://www.isa-afp.org/entries/Interpreter_Optimizations.html Martin Desharnais 07 Dec 2020 00:00:00 +0000 This Isabelle/HOL formalization builds on the <em>VeriComp</em> entry of the <em>Archive of Formal Proofs</em> to provide the following contributions: <ul> <li>an operational semantics for a realistic virtual machine (Std) for dynamically typed programming languages;</li> <li>the formalization of an inline caching optimization (Inca), a proof of bisimulation with (Std), and a compilation function;</li> <li>the formalization of an unboxing optimization (Ubx), a proof of bisimulation with (Inca), and a simple compilation function.</li> </ul> This formalization was described in the CPP 2021 paper <em>Towards Efficient and Verified Virtual Machines for Dynamic Languages</em> The Relational Method with Message Anonymity for the Verification of Cryptographic Protocols https://www.isa-afp.org/entries/Relational_Method.html https://www.isa-afp.org/entries/Relational_Method.html Pasquale Noce 05 Dec 2020 00:00:00 +0000 This paper introduces a new method for the formal verification of cryptographic protocols, the relational method, derived from Paulson's inductive method by means of some enhancements aimed at streamlining formal definitions and proofs, specially for protocols using public key cryptography. Moreover, this paper proposes a method to formalize a further security property, message anonymity, in addition to message confidentiality and authenticity. The relational method, including message anonymity, is then applied to the verification of a sample authentication protocol, comprising Password Authenticated Connection Establishment (PACE) with Chip Authentication Mapping followed by the explicit verification of an additional password over the PACE secure channel. Isabelle Marries Dirac: a Library for Quantum Computation and Quantum Information https://www.isa-afp.org/entries/Isabelle_Marries_Dirac.html https://www.isa-afp.org/entries/Isabelle_Marries_Dirac.html Anthony Bordg, Hanna Lachnitt, Yijun He 22 Nov 2020 00:00:00 +0000 This work is an effort to formalise some quantum algorithms and results in quantum information theory. Formal methods being critical for the safety and security of algorithms and protocols, we foresee their widespread use for quantum computing in the future. We have developed a large library for quantum computing in Isabelle based on a matrix representation for quantum circuits, successfully formalising the no-cloning theorem, quantum teleportation, Deutsch's algorithm, the Deutsch-Jozsa algorithm and the quantum Prisoner's Dilemma. The HOL-CSP Refinement Toolkit https://www.isa-afp.org/entries/CSP_RefTK.html https://www.isa-afp.org/entries/CSP_RefTK.html Safouan Taha, Burkhart Wolff, Lina Ye 19 Nov 2020 00:00:00 +0000 We use a formal development for CSP, called HOL-CSP2.0, to analyse a family of refinement notions, comprising classic and new ones. This analysis enables to derive a number of properties that allow to deepen the understanding of these notions, in particular with respect to specification decomposition principles for the case of infinite sets of events. The established relations between the refinement relations help to clarify some obscure points in the CSP literature, but also provide a weapon for shorter refinement proofs. Furthermore, we provide a framework for state-normalisation allowing to formally reason on parameterised process architectures. As a result, we have a modern environment for formal proofs of concurrent systems that allow for the combination of general infinite processes with locally finite ones in a logically safe way. We demonstrate these verification-techniques for classical, generalised examples: The CopyBuffer for arbitrary data and the Dijkstra's Dining Philosopher Problem of arbitrary size. Verified SAT-Based AI Planning https://www.isa-afp.org/entries/Verified_SAT_Based_AI_Planning.html https://www.isa-afp.org/entries/Verified_SAT_Based_AI_Planning.html Mohammad Abdulaziz, Friedrich Kurz 29 Oct 2020 00:00:00 +0000 We present an executable formally verified SAT encoding of classical AI planning that is based on the encodings by Kautz and Selman and the one by Rintanen et al. The encoding was experimentally tested and shown to be usable for reasonably sized standard AI planning benchmarks. We also use it as a reference to test a state-of-the-art SAT-based planner, showing that it sometimes falsely claims that problems have no solutions of certain lengths. The formalisation in this submission was described in an independent publication. AI Planning Languages Semantics https://www.isa-afp.org/entries/AI_Planning_Languages_Semantics.html https://www.isa-afp.org/entries/AI_Planning_Languages_Semantics.html Mohammad Abdulaziz, Peter Lammich 29 Oct 2020 00:00:00 +0000 This is an Isabelle/HOL formalisation of the semantics of the multi-valued planning tasks language that is used by the planning system Fast-Downward, the STRIPS fragment of the Planning Domain Definition Language (PDDL), and the STRIPS soundness meta-theory developed by Vladimir Lifschitz. It also contains formally verified checkers for checking the well-formedness of problems specified in either language as well the correctness of potential solutions. The formalisation in this entry was described in an earlier publication. A Sound Type System for Physical Quantities, Units, and Measurements https://www.isa-afp.org/entries/Physical_Quantities.html https://www.isa-afp.org/entries/Physical_Quantities.html Simon Foster, Burkhart Wolff 20 Oct 2020 00:00:00 +0000 The present Isabelle theory builds a formal model for both the International System of Quantities (ISQ) and the International System of Units (SI), which are both fundamental for physics and engineering. Both the ISQ and the SI are deeply integrated into Isabelle's type system. Quantities are parameterised by dimension types, which correspond to base vectors, and thus only quantities of the same dimension can be equated. Since the underlying "algebra of quantities" induces congruences on quantity and SI types, specific tactic support is developed to capture these. Our construction is validated by a test-set of known equivalences between both quantities and SI units. Moreover, the presented theory can be used for type-safe conversions between the SI system and others, like the British Imperial System (BIS). Finite Map Extras https://www.isa-afp.org/entries/Finite-Map-Extras.html https://www.isa-afp.org/entries/Finite-Map-Extras.html Javier Díaz 12 Oct 2020 00:00:00 +0000 This entry includes useful syntactic sugar, new operators and functions, and their associated lemmas for finite maps which currently are not present in the standard Finite_Map theory. A Formal Model of the Safely Composable Document Object Model with Shadow Roots https://www.isa-afp.org/entries/Shadow_SC_DOM.html https://www.isa-afp.org/entries/Shadow_SC_DOM.html Achim D. Brucker, Michael Herzberg 28 Sep 2020 00:00:00 +0000 In this AFP entry, we extend our formalization of the safely composable DOM with Shadow Roots. This is a proposal for Shadow Roots with stricter safety guarantess than the standard compliant formalization (see "Shadow DOM"). Shadow Roots are a recent proposal of the web community to support a component-based development approach for client-side web applications. Shadow roots are a significant extension to the DOM standard and, as web standards are condemned to be backward compatible, such extensions often result in complex specification that may contain unwanted subtleties that can be detected by a formalization. Our Isabelle/HOL formalization is, in the sense of object-orientation, an extension of our formalization of the core DOM and enjoys the same basic properties, i.e., it is extensible, i.e., can be extended without the need of re-proving already proven properties and executable, i.e., we can generate executable code from our specification. We exploit the executability to show that our formalization complies to the official standard of the W3C, respectively, the WHATWG. A Formal Model of the Document Object Model with Shadow Roots https://www.isa-afp.org/entries/Shadow_DOM.html https://www.isa-afp.org/entries/Shadow_DOM.html Achim D. Brucker, Michael Herzberg 28 Sep 2020 00:00:00 +0000 In this AFP entry, we extend our formalization of the core DOM with Shadow Roots. Shadow roots are a recent proposal of the web community to support a component-based development approach for client-side web applications. Shadow roots are a significant extension to the DOM standard and, as web standards are condemned to be backward compatible, such extensions often result in complex specification that may contain unwanted subtleties that can be detected by a formalization. Our Isabelle/HOL formalization is, in the sense of object-orientation, an extension of our formalization of the core DOM and enjoys the same basic properties, i.e., it is extensible, i.e., can be extended without the need of re-proving already proven properties and executable, i.e., we can generate executable code from our specification. We exploit the executability to show that our formalization complies to the official standard of the W3C, respectively, the WHATWG. A Formalization of Safely Composable Web Components https://www.isa-afp.org/entries/SC_DOM_Components.html https://www.isa-afp.org/entries/SC_DOM_Components.html Achim D. Brucker, Michael Herzberg 28 Sep 2020 00:00:00 +0000 While the (safely composable) DOM with shadow trees provide the technical basis for defining web components, it does neither defines the concept of web components nor specifies the safety properties that web components should guarantee. Consequently, the standard also does not discuss how or even if the methods for modifying the DOM respect component boundaries. In AFP entry, we present a formally verified model of safely composable web components and define safety properties which ensure that different web components can only interact with each other using well-defined interfaces. Moreover, our verification of the application programming interface (API) of the DOM revealed numerous invariants that implementations of the DOM API need to preserve to ensure the integrity of components. In comparison to the strict standard compliance formalization of Web Components in the AFP entry "DOM_Components", the notion of components in this entry (based on "SC_DOM" and "Shadow_SC_DOM") provides much stronger safety guarantees. A Formalization of Web Components https://www.isa-afp.org/entries/DOM_Components.html https://www.isa-afp.org/entries/DOM_Components.html Achim D. Brucker, Michael Herzberg 28 Sep 2020 00:00:00 +0000 While the DOM with shadow trees provide the technical basis for defining web components, the DOM standard neither defines the concept of web components nor specifies the safety properties that web components should guarantee. Consequently, the standard also does not discuss how or even if the methods for modifying the DOM respect component boundaries. In AFP entry, we present a formally verified model of web components and define safety properties which ensure that different web components can only interact with each other using well-defined interfaces. Moreover, our verification of the application programming interface (API) of the DOM revealed numerous invariants that implementations of the DOM API need to preserve to ensure the integrity of components. The Safely Composable DOM https://www.isa-afp.org/entries/Core_SC_DOM.html https://www.isa-afp.org/entries/Core_SC_DOM.html Achim D. Brucker, Michael Herzberg 28 Sep 2020 00:00:00 +0000 In this AFP entry, we formalize the core of the Safely Composable Document Object Model (SC DOM). The SC DOM improve the standard DOM (as formalized in the AFP entry "Core DOM") by strengthening the tree boundaries set by shadow roots: in the SC DOM, the shadow root is a sub-class of the document class (instead of a base class). This modifications also results in changes to some API methods (e.g., getOwnerDocument) to return the nearest shadow root rather than the document root. As a result, many API methods that, when called on a node inside a shadow tree, would previously ``break out'' and return or modify nodes that are possibly outside the shadow tree, now stay within its boundaries. This change in behavior makes programs that operate on shadow trees more predictable for the developer and allows them to make more assumptions about other code accessing the DOM. Syntax-Independent Logic Infrastructure https://www.isa-afp.org/entries/Syntax_Independent_Logic.html https://www.isa-afp.org/entries/Syntax_Independent_Logic.html Andrei Popescu, Dmitriy Traytel 16 Sep 2020 00:00:00 +0000 We formalize a notion of logic whose terms and formulas are kept abstract. In particular, logical connectives, substitution, free variables, and provability are not defined, but characterized by their general properties as locale assumptions. Based on this abstract characterization, we develop further reusable reasoning infrastructure. For example, we define parallel substitution (along with proving its characterizing theorems) from single-point substitution. Similarly, we develop a natural deduction style proof system starting from the abstract Hilbert-style one. These one-time efforts benefit different concrete logics satisfying our locales' assumptions. We instantiate the syntax-independent logic infrastructure to Robinson arithmetic (also known as Q) in the AFP entry <a href="https://www.isa-afp.org/entries/Robinson_Arithmetic.html">Robinson_Arithmetic</a> and to hereditarily finite set theory in the AFP entries <a href="https://www.isa-afp.org/entries/Goedel_HFSet_Semantic.html">Goedel_HFSet_Semantic</a> and <a href="https://www.isa-afp.org/entries/Goedel_HFSet_Semanticless.html">Goedel_HFSet_Semanticless</a>, which are part of our formalization of G&ouml;del's Incompleteness Theorems described in our CADE-27 paper <a href="https://dx.doi.org/10.1007/978-3-030-29436-6_26">A Formally Verified Abstract Account of Gödel's Incompleteness Theorems</a>. Robinson Arithmetic https://www.isa-afp.org/entries/Robinson_Arithmetic.html https://www.isa-afp.org/entries/Robinson_Arithmetic.html Andrei Popescu, Dmitriy Traytel 16 Sep 2020 00:00:00 +0000 We instantiate our syntax-independent logic infrastructure developed in <a href="https://www.isa-afp.org/entries/Syntax_Independent_Logic.html">a separate AFP entry</a> to the FOL theory of Robinson arithmetic (also known as Q). The latter was formalised using Nominal Isabelle by adapting <a href="https://www.isa-afp.org/entries/Incompleteness.html">Larry Paulson’s formalization of the Hereditarily Finite Set theory</a>. - - An Abstract Formalization of Gödel's Incompleteness Theorems - https://www.isa-afp.org/entries/Goedel_Incompleteness.html - https://www.isa-afp.org/entries/Goedel_Incompleteness.html - Andrei Popescu, Dmitriy Traytel - 16 Sep 2020 00:00:00 +0000 - -We present an abstract formalization of G&ouml;del's -incompleteness theorems. We analyze sufficient conditions for the -theorems' applicability to a partially specified logic. Our -abstract perspective enables a comparison between alternative -approaches from the literature. These include Rosser's variation -of the first theorem, Jeroslow's variation of the second theorem, -and the Swierczkowski&ndash;Paulson semantics-based approach. This -AFP entry is the main entry point to the results described in our -CADE-27 paper <a -href="https://dx.doi.org/10.1007/978-3-030-29436-6_26">A -Formally Verified Abstract Account of Gödel's Incompleteness -Theorems</a>. As part of our abstract formalization's -validation, we instantiate our locales twice in the separate AFP -entries <a -href="https://www.isa-afp.org/entries/Goedel_HFSet_Semantic.html">Goedel_HFSet_Semantic</a> -and <a -href="https://www.isa-afp.org/entries/Goedel_HFSet_Semanticless.html">Goedel_HFSet_Semanticless</a>. - diff --git a/web/statistics.html b/web/statistics.html --- a/web/statistics.html +++ b/web/statistics.html @@ -1,302 +1,302 @@ Archive of Formal Proofs

 

 

 

Home
About
Submission
Updating Entries
Using Entries
Search
Statistics
Index
Download

 

 

 

Statistics

 

Statistics

- - - - + + + +
Number of Articles:588
Number of Authors:375
Number of lemmas:~164,600
Lines of Code:~2,874,700
Number of Articles:589
Number of Authors:377
Number of lemmas:~165,000
Lines of Code:~2,891,800

Most used AFP articles:

+ + + + - - - - + + + + - - - -
NameUsed by ? articles
1. List-Index 17
2. Coinductive 12
Collections 12
Regular-Sets 12
Show12
3. Landau_Symbols 11
Show11
4.Jordan_Normal_Form10
Polynomial_Factorization 10
5. Abstract-Rewriting 9
Automatic_Refinement 9
Deriving 9
Jordan_Normal_Form9

Growth in number of articles:

Growth in lines of code:

Growth in number of authors:

Size of articles:
\ No newline at end of file diff --git a/web/topics.html b/web/topics.html --- a/web/topics.html +++ b/web/topics.html @@ -1,947 +1,948 @@ Archive of Formal Proofs

 

 

 

Home
About
Submission
Updating Entries
Using Entries
Search
Statistics
Index
Download

 

 

 

Index by Topic

 

Computer science

Artificial intelligence

AI_Planning_Languages_Semantics   Verified_SAT_Based_AI_Planning  

Automata and formal languages

Partial_Order_Reduction   C2KA_DistributedSystems   Posix-Lexing   LocalLexing   KBPs   Regular-Sets   Regex_Equivalence   MSO_Regex_Equivalence   Formula_Derivatives   Myhill-Nerode   Universal_Turing_Machine   CYK   Presburger-Automata   Functional-Automata   Statecharts   Stuttering_Equivalence   Coinductive_Languages   Tree-Automata   Kleene_Algebra   KAT_and_DRA   KAD   Regular_Algebras   Markov_Models   Probabilistic_System_Zoo   CAVA_Automata   LTL   LTL_to_GBA   CAVA_LTL_Modelchecker   Probabilistic_Timed_Automata   Finite_Automata_HF   LTL_to_DRA   Timed_Automata   Stochastic_Matrices   Buchi_Complementation   Transition_Systems_and_Automata   Factored_Transition_System_Bounding   LTL_Master_Theorem   MFOTL_Monitor   Adaptive_State_Counting   MFODL_Monitor_Optimized   LTL_Normal_Form   Extended_Finite_State_Machines   Extended_Finite_State_Machine_Inference  

Algorithms

Knuth_Morris_Pratt   Probabilistic_While   Comparison_Sort_Lower_Bound   Quick_Sort_Cost   TortoiseHare   Selection_Heap_Sort   VerifyThis2018   CYK   Boolean_Expression_Checkers   Efficient-Mergesort   SATSolverVerification   MuchAdoAboutTwo   First_Order_Terms   Monad_Memo_DP   Hidden_Markov_Models   Imperative_Insertion_Sort   Formal_SSA   ROBDD   Median_Of_Medians_Selection   Fisher_Yates   Optimal_BST   IMP2   Auto2_Imperative_HOL   List_Inversions   IMP2_Binary_Heap   MFOTL_Monitor   Adaptive_State_Counting   Generic_Join   VerifyThis2019   Generalized_Counting_Sort   MFODL_Monitor_Optimized   Sliding_Window_Algorithm   PAC_Checker   Graph: DFS_Framework   Prpu_Maxflow   Floyd_Warshall   Roy_Floyd_Warshall   Dijkstra_Shortest_Path   EdmondsKarp_Maxflow   Depth-First-Search   GraphMarkingIBP   Transitive-Closure   Transitive-Closure-II   Gabow_SCC   Kruskal   Prim_Dijkstra_Simple   Relational_Minimum_Spanning_Trees   Distributed: DiskPaxos   GenClock   ClockSynchInst   Heard_Of   Consensus_Refined   Abortable_Linearizable_Modules   IMAP-CRDT   CRDT   Chandy_Lamport   OpSets   Stellar_Quorums   WOOT_Strong_Eventual_Consistency   Concurrent: ConcurrentGC   Online: List_Update   Geometry: Closest_Pair_Points   Approximation: Approximation_Algorithms   Mathematical: FFT   Gauss-Jordan-Elim-Fun   UpDown_Scheme   Polynomials   Gauss_Jordan   Echelon_Form   QR_Decomposition   Hermite   Groebner_Bases   Diophantine_Eqns_Lin_Hom   Taylor_Models   LLL_Basis_Reduction   Signature_Groebner   Smith_Normal_Form   Safe_Distance   + Modular_arithmetic_LLL_and_HNF_algorithms   Optimization: Simplex   Quantum computing: Isabelle_Marries_Dirac   Projective_Measurements  

Concurrency

FLP   Concurrent_Ref_Alg   Concurrent_Revisions   Store_Buffer_Reduction   TESL_Language   Process calculi: Noninterference_Generic_Unwinding   AODV   AWN   CCS   Pi_Calculus   Psi_Calculi   Encodability_Process_Calculi   Circus   Noninterference_Sequential_Composition   Noninterference_Concurrent_Composition   Modal_Logics_for_NTS   HOL-CSP   CSP_RefTK  

Data structures

Generic_Deriving   Random_BSTs   Randomised_BSTs   List_Interleaving   Refine_Imperative_HOL   Amortized_Complexity   Dynamic_Tables   AVL-Trees   BDD   BinarySearchTree   Splay_Tree   Root_Balanced_Tree   Skew_Heap   Pairing_Heap   Priority_Queue_Braun   Binomial-Queues   Binomial-Heaps   Finger-Trees   Trie   FinFun   Collections   Containers   FileRefinement   Datatype_Order_Generator   Deriving   List-Index   List-Infinite   Matrix   Matrix_Tensor   Huffman   Lazy-Lists-II   IEEE_Floating_Point   Native_Word   XML   ROBDD   IMAP-CRDT   Word_Lib   CRDT   KD_Tree   Taylor_Models   Treaps   Skip_Lists   Weight_Balanced_Trees   OpSets   Optimal_BST   Core_DOM   Core_SC_DOM   Shadow_SC_DOM   SC_DOM_Components   Auto2_Imperative_HOL   IMP2_Binary_Heap   Priority_Search_Trees   Interval_Arithmetic_Word32   ADS_Functor   Relational_Disjoint_Set_Forests   Shadow_DOM   DOM_Components   Finite-Map-Extras   Hood_Melville_Queue   BTree  

Functional programming

Optics   CryptHOL   Probabilistic_While   Monad_Normalisation   Monomorphic_Monad   Show   Certification_Monads   Partial_Function_MR   Lifting_Definition_Option   Coinductive   Stream-Fusion   Tycon   Monad_Memo_DP   XML   Tail_Recursive_Functions   Stream_Fusion_Code   Applicative_Lifting   HOLCF-Prelude   BNF_CC   Binding_Syntax_Theory   Generalized_Counting_Sort   Hello_World   BirdKMP  

Hardware

SPARCv8  

Machine learning

Deep_Learning   Inductive_Inference  

Networks

UPF_Firewall   IP_Addresses   Simple_Firewall   Iptables_Semantics   Routing   LOFT  

Programming languages

Clean   Decl_Sem_Fun_PL   Language definitions: CakeML   WebAssembly   pGCL   GPU_Kernel_PL   LightweightJava   CoreC++   FeatherweightJava   Jinja   JinjaThreads   Locally-Nameless-Sigma   AutoFocus-Stream   FocusStreamsCaseStudies   Isabelle_Meta_Model   Simpl   Complx   Safe_OCL   Isabelle_C   JinjaDCI   Lambda calculi: Higher_Order_Terms   Launchbury   PCF   POPLmark-deBruijn   Lam-ml-Normalization   LambdaMu   Binding_Syntax_Theory   LambdaAuth   Type systems: Name_Carrying_Type_Inference   MiniML   Possibilistic_Noninterference   SIFUM_Type_Systems   Dependent_SIFUM_Type_Systems   Strong_Security   WHATandWHERE_Security   VolpanoSmith   Physical_Quantities   Logics: ConcurrentIMP   Refine_Monadic   Automatic_Refinement   MonoBoolTranAlgebra   Simpl   Separation_Algebra   Separation_Logic_Imperative_HOL   Relational-Incorrectness-Logic   Abstract-Hoare-Logics   Kleene_Algebra   KAT_and_DRA   KAD   BytecodeLogicJmlTypes   DataRefinementIBP   RefinementReactive   SIFPL   TLA   Ribbon_Proofs   Separata   Complx   Differential_Dynamic_Logic   Hoare_Time   IMP2   UTP   QHLProver   Differential_Game_Logic   Compiling: CakeML_Codegen   Compiling-Exceptions-Correctly   NormByEval   Density_Compiler   VeriComp   Static analysis: RIPEMD-160-SPARK   Program-Conflict-Analysis   Shivers-CFA   Slicing   HRB-Slicing   InfPathElimination   Abs_Int_ITP2012   Transformations: Call_Arity   Refine_Imperative_HOL   WorkerWrapper   Monad_Memo_DP   Formal_SSA   Minimal_SSA   Misc: JiveDataStoreModel   Pop_Refinement   Case_Labeling   Interpreter_Optimizations  

Security

Multi_Party_Computation   Noninterference_Generic_Unwinding   Noninterference_Ipurge_Unwinding   Relational_Method   UPF   UPF_Firewall   CISC-Kernel   Noninterference_CSP   Key_Agreement_Strong_Adversaries   Security_Protocol_Refinement   Attack_Trees   Inductive_Confidentiality   Possibilistic_Noninterference   SIFUM_Type_Systems   Dependent_SIFUM_Type_Systems   Dependent_SIFUM_Refinement   Relational-Incorrectness-Logic   Strong_Security   WHATandWHERE_Security   VolpanoSmith   SIFPL   HotelKeyCards   InformationFlowSlicing   InformationFlowSlicing_Inter   CryptoBasedCompositionalProperties   Probabilistic_Noninterference   HyperCTL   Bounded_Deducibility_Security   Network_Security_Policy_Verification   Noninterference_Inductive_Unwinding   Password_Authentication_Protocol   Noninterference_Sequential_Composition   Noninterference_Concurrent_Composition   SPARCv8   Modular_Assembly_Kit_Security   LambdaAuth   Stateful_Protocol_Composition_and_Typing   Automated_Stateful_Protocol_Verification   Cryptography: Game_Based_Crypto   Sigma_Commit_Crypto   CryptHOL   Constructive_Cryptography   RSAPSS   Elliptic_Curves_Group_Law  

Semantics

Launchbury   Clean   Transformer_Semantics   HOL-CSP   QHLProver   TESL_Language   Isabelle_C   CSP_RefTK  

System description languages

Circus   ComponentDependencies   Promela   Featherweight_OCL   DynamicArchitectures   Architectural_Design_Patterns   TESL_Language  

Logic

Philosophical aspects

GoedelGod   Types_Tableaus_and_Goedels_God   GewirthPGCProof   Lowe_Ontological_Argument   AnselmGod   PLM   Aristotles_Assertoric_Syllogistic   Mereology  

General logic

Topological_Semantics   Classical propositional logic: Free-Boolean-Algebra   Classical first-order logic: FOL-Fitting   Decidability of theories: MSO_Regex_Equivalence   Formula_Derivatives   Presburger-Automata   LinearQuantifierElim   Mechanization of proofs: Boolean_Expression_Checkers   Verified-Prover   Sort_Encodings   PropResPI   Resolution_FOL   FOL_Harrison   Ordered_Resolution_Prover   Functional_Ordered_Resolution_Prover   Binding_Syntax_Theory   Saturation_Framework   Saturation_Framework_Extensions   Lambda calculus: LambdaMu   Logics of knowledge and belief: Epistemic_Logic   Blue_Eyes   Temporal logic: Nat-Interval-Logic   LTL   HyperCTL   Allen_Calculus   MFOTL_Monitor   LTL_Normal_Form   Modal logic: Modal_Logics_for_NTS   Differential_Dynamic_Logic   Hybrid_Multi_Lane_Spatial_Logic   Hybrid_Logic   MFODL_Monitor_Optimized   Paraconsistent logics: Paraconsistency  

Computability

Universal_Turing_Machine   Recursion-Theory-I   Inductive_Inference   Minsky_Machines  

Set theory

Ordinal   Ordinals_and_Cardinals   HereditarilyFinite   ZFC_in_HOL   Forcing   Delta_System_Lemma   Recursion-Addition   Ordinal_Partitions  

Proof theory

Propositional_Proof_Systems   Completeness   SequentInvertibility   Incompleteness   Abstract_Completeness   SuperCalc   Incredible_Proof_Machine   Surprise_Paradox   Abstract_Soundness   Syntax_Independent_Logic   Goedel_Incompleteness   Goedel_HFSet_Semantic   Goedel_HFSet_Semanticless   Robinson_Arithmetic   FOL_Seq_Calc1  

Rewriting

CakeML_Codegen   Monad_Normalisation   Lambda_Free_RPOs   Lambda_Free_KBOs   Lambda_Free_EPO   Nested_Multisets_Ordinals   Abstract-Rewriting   First_Order_Terms   Decreasing-Diagrams   Decreasing-Diagrams-II   Rewriting_Z   Graph_Saturation   Goodstein_Lambda   Knuth_Bendix_Order  

Mathematics

Order

LatticeProperties   Stone_Algebras   Allen_Calculus   Order_Lattice_Props   Complete_Non_Orders   Szpilrajn  

Algebra

Optics   Subresultants   Buildings   Algebraic_VCs   C2KA_DistributedSystems   Multirelations   Residuated_Lattices   PseudoHoops   Impossible_Geometry   Gauss-Jordan-Elim-Fun   Matrix_Tensor   Kleene_Algebra   KAT_and_DRA   KAD   Regular_Algebras   Free-Groups   CofGroups   Group-Ring-Module   Robbins-Conjecture   Valuation   Rank_Nullity_Theorem   Polynomials   Relation_Algebra   PSemigroupsConvolution   Secondary_Sylow   Jordan_Hoelder   Cayley_Hamilton   VectorSpace   Echelon_Form   QR_Decomposition   Hermite   Rep_Fin_Groups   Jordan_Normal_Form   Algebraic_Numbers   Polynomial_Interpolation   Polynomial_Factorization   Perron_Frobenius   Stochastic_Matrices   Groebner_Bases   Nullstellensatz   Mason_Stothers   Berlekamp_Zassenhaus   Stone_Relation_Algebras   Stone_Kleene_Relation_Algebras   Orbit_Stabiliser   Dirichlet_L   Symmetric_Polynomials   Taylor_Models   LLL_Basis_Reduction   LLL_Factorization   Localization_Ring   Quaternions   Octonions   Aggregation_Algebras   Signature_Groebner   Quantales   Transformer_Semantics   Farkas   Groebner_Macaulay   Linear_Inequalities   Linear_Programming   Jacobson_Basic_Algebra   Hybrid_Systems_VCs   Subset_Boolean_Algebras   Power_Sum_Polynomials   Formal_Puiseux_Series   Matrices_for_ODEs   Smith_Normal_Form  

Analysis

Banach_Steinhaus   Fourier   E_Transcendental   Liouville_Numbers   Descartes_Sign_Rule   Euler_MacLaurin   Real_Impl   Lower_Semicontinuous   Affine_Arithmetic   Laplace_Transform   Cauchy   Integration   Ordinary_Differential_Equations   Polynomials   Sqrt_Babylonian   Sturm_Sequences   Sturm_Tarski   Special_Function_Bounds   Landau_Symbols   Error_Function   Akra_Bazzi   Zeta_Function   Linear_Recurrences   Lambert_W   Cartan_FP   Deep_Learning   Stirling_Formula   Lp   Bernoulli   Winding_Number_Eval   Count_Complex_Roots   Taylor_Models   Green   Irrationality_J_Hancl   Budan_Fourier   Smooth_Manifolds   Transcendence_Series_Hancl_Rucki   Hybrid_Systems_VCs   Poincare_Bendixson   Matrices_for_ODEs   Irrational_Series_Erdos_Straus  

Probability theory

DiscretePricing   CryptHOL   Constructive_Cryptography   Probabilistic_While   Markov_Models   Density_Compiler   Probabilistic_Timed_Automata   Hidden_Markov_Models   Random_Graph_Subgraph_Threshold   Ergodic_Theory   Source_Coding_Theorem   Buffons_Needle   Laws_of_Large_Numbers  

Number theory

Arith_Prog_Rel_Primes   Pell   Minkowskis_Theorem   E_Transcendental   Pi_Transcendental   Hermite_Lindemann   Liouville_Numbers   Prime_Harmonic_Series   Fermat3_4   Perfect-Number-Thm   SumSquares   Lehmer   Pratt_Certificate   Dirichlet_Series   Gauss_Sums   Zeta_Function   Stern_Brocot   Bertrands_Postulate   Bernoulli   Diophantine_Eqns_Lin_Hom   Dirichlet_L   Mersenne_Primes   Irrationality_J_Hancl   Prime_Number_Theorem   Probabilistic_Prime_Tests   Prime_Distribution_Elementary   Transcendence_Series_Hancl_Rucki   Zeta_3_Irrational   Furstenberg_Topology   Lucas_Theorem   Gaussian_Integers   Irrational_Series_Erdos_Straus   Amicable_Numbers  

Games and economics

DiscretePricing   ArrowImpossibilityGS   SenSocialChoice   Vickrey_Clarke_Groves   Parity_Game   First_Welfare_Theorem   Randomised_Social_Choice   SDS_Impossibility   Stable_Matching   Fishburn_Impossibility   Neumann_Morgenstern_Utility  

Geometry

Complex_Geometry   Poincare_Disc   Minkowskis_Theorem   Buildings   Chord_Segments   Triangle   Impossible_Geometry   Tarskis_Geometry   IsaGeoCoq   General-Triangle   Nullstellensatz   Ptolemys_Theorem   Buffons_Needle   Stewart_Apollonius   Gromov_Hyperbolicity   Projective_Geometry   Quaternions   Octonions  

Topology

Topology   Knot_Theory   Kuratowski_Closure_Complement   Smooth_Manifolds  

Graph theory

Flow_Networks   Prpu_Maxflow   MFMC_Countable   ShortestPath   Gabow_SCC   Graph_Theory   Planarity_Certificates   Max-Card-Matching   Girth_Chromatic   Random_Graph_Subgraph_Threshold   Flyspeck-Tame   Koenigsberg_Friendship   Tree_Decomposition   Menger   Parity_Game   Factored_Transition_System_Bounding   Graph_Saturation   Relational_Paths  

Combinatorics

Card_Equiv_Relations   Twelvefold_Way   Card_Multisets   Card_Partitions   Card_Number_Partitions   Well_Quasi_Orders   Marriage   Bondy   Ramsey-Infinite   Derangements   Euler_Partition   Discrete_Summation   Open_Induction   Latin_Square   Bell_Numbers_Spivey   Catalan_Numbers   Falling_Factorial_Sum   Matroids   Delta_System_Lemma   Nash_Williams   Ordinal_Partitions   Sunflowers  

Category theory

Category3   MonoidalCategory   Category   Category2   AxiomaticCategoryTheory   Bicategory  

Physics

No_FTL_observers   Safe_Distance   Physical_Quantities   Quantum information: Isabelle_Marries_Dirac   Projective_Measurements  

Misc

FunWithFunctions   FunWithTilings   IMO2019  

Tools

Monad_Normalisation   Constructor_Funs   Lazy_Case   Dict_Construction   Case_Labeling   DPT-SAT-Solver   Nominal2   Separata   Proof_Strategy_Language   Diophantine_Eqns_Lin_Hom   BNF_Operations   BNF_CC   Auto2_HOL   Isabelle_C   Automated_Stateful_Protocol_Verification  
\ No newline at end of file