diff --git a/web/entries/Independence_CH.html b/web/entries/Independence_CH.html --- a/web/entries/Independence_CH.html +++ b/web/entries/Independence_CH.html @@ -1,200 +1,200 @@ The Independence of the Continuum Hypothesis in Isabelle/ZF - Archive of Formal Proofs

 

 

 

Home
About
Submission
Updating Entries
Using Entries
Search
Statistics
Index
Download

 

 

 

The Independence of the Continuum Hypothesis in Isabelle/ZF

 

Title: The Independence of the Continuum Hypothesis in Isabelle/ZF
Authors: Emmanuel Gunther (gunther /at/ famaf /dot/ unc /dot/ edu /dot/ ar), Miguel Pagano, Pedro Sánchez Terraf and - and Matías Steinberg (matias /dot/ steinberg /at/ mi /dot/ unc /dot/ edu /dot/ ar) + Matías Steinberg (matias /dot/ steinberg /at/ mi /dot/ unc /dot/ edu /dot/ ar)
Submission date: 2022-03-06
Abstract: We redeveloped our formalization of forcing in the set theory framework of Isabelle/ZF. Under the assumption of the existence of a countable transitive model of ZFC, we construct proper generic extensions that satisfy the Continuum Hypothesis and its negation.
BibTeX: 
@article{Independence_CH-AFP,
-  author  = {Emmanuel Gunther and Miguel Pagano and Pedro Sánchez Terraf and and Matías Steinberg},
+  author  = {Emmanuel Gunther and Miguel Pagano and Pedro Sánchez Terraf and Matías Steinberg},
   title   = {The Independence of the Continuum Hypothesis in Isabelle/ZF},
   journal = {Archive of Formal Proofs},
   month   = mar,
   year    = 2022,
   note    = {\url{https://isa-afp.org/entries/Independence_CH.html},
             Formal proof development},
   ISSN    = {2150-914x},
 }
License: BSD License
Depends on: Transitive_Models

Proof outline
Proof document
Browse theories
Download this entry
Older releases: None
\ No newline at end of file diff --git a/web/entries/Sophomores_Dream.html b/web/entries/Sophomores_Dream.html new file mode 100644 --- /dev/null +++ b/web/entries/Sophomores_Dream.html @@ -0,0 +1,186 @@ + + + + +The Sophomore's Dream - Archive of Formal Proofs + + + + + + + + + + + + + + + + + + + + + + + + +
+

 

+ + + +

 

+

 

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

 

+

 

+		 +
+

 

+

The + + Sophomore's + + Dream + +

+

 

+ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
Title:The Sophomore's Dream
+ Author: + + Manuel Eberl +
Submission date:2022-04-10
Abstract: +

This article provides a brief formalisation of the two +equations known as the Sophomore's Dream, +first discovered by Johann Bernoulli in 1697:

\[\int_0^1 +x^{-x}\,\text{d}x = \sum_{n=1}^\infty n^{-n} \quad\text{and}\quad +\int_0^1 x^x\,\text{d}x = -\sum_{n=1}^\infty (-n)^{-n}\]
BibTeX: + 
@article{Sophomores_Dream-AFP,
+  author  = {Manuel Eberl},
+  title   = {The Sophomore's Dream},
+  journal = {Archive of Formal Proofs},
+  month   = apr,
+  year    = 2022,
+  note    = {\url{https://isa-afp.org/entries/Sophomores_Dream.html},
+            Formal proof development},
+  ISSN    = {2150-914x},
+}
+
License:BSD License
+ +

+ + + + + + + + + + + + + + + + +
+ Proof outline
+ Proof document +
+ Browse theories +
+ Download this entry +
Older releases: + None +
+ +
+
+ + + + + + \ No newline at end of file diff --git a/web/entries/Transitive_Models.html b/web/entries/Transitive_Models.html --- a/web/entries/Transitive_Models.html +++ b/web/entries/Transitive_Models.html @@ -1,200 +1,200 @@ Transitive Models of Fragments of ZFC - Archive of Formal Proofs

 

 

 

Home
About
Submission
Updating Entries
Using Entries
Search
Statistics
Index
Download

 

 

 

Transitive Models of Fragments of ZFC

 

Title: Transitive Models of Fragments of ZFC
Authors: Emmanuel Gunther (gunther /at/ famaf /dot/ unc /dot/ edu /dot/ ar), Miguel Pagano, Pedro Sánchez Terraf and - and Matías Steinberg (matias /dot/ steinberg /at/ mi /dot/ unc /dot/ edu /dot/ ar) + Matías Steinberg (matias /dot/ steinberg /at/ mi /dot/ unc /dot/ edu /dot/ ar)
Submission date: 2022-03-03
Abstract: We extend the ZF-Constructibility library by relativizing theories of the Isabelle/ZF and Delta System Lemma sessions to a transitive class. We also relativize Paulson's work on Aleph and our former treatment of the Axiom of Dependent Choices. This work is a prerrequisite to our formalization of the independence of the Continuum Hypothesis.
BibTeX: 
@article{Transitive_Models-AFP,
-  author  = {Emmanuel Gunther and Miguel Pagano and Pedro Sánchez Terraf and and Matías Steinberg},
+  author  = {Emmanuel Gunther and Miguel Pagano and Pedro Sánchez Terraf and Matías Steinberg},
   title   = {Transitive Models of Fragments of ZFC},
   journal = {Archive of Formal Proofs},
   month   = mar,
   year    = 2022,
   note    = {\url{https://isa-afp.org/entries/Transitive_Models.html},
             Formal proof development},
   ISSN    = {2150-914x},
 }
License: BSD License
Depends on: Delta_System_Lemma
Used by: Independence_CH

Proof outline
Proof document
Browse theories
Download this entry
Older releases: None
\ 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,6186 +1,6194 @@ 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.

 

 

+ + +
2022
2022-05-08: Clique is not solvable by monotone circuits of polynomial size
Author: René Thiemann
2022-04-21: Fisher's Inequality: Linear Algebraic Proof Techniques for Combinatorics
Authors: Chelsea Edmonds and Lawrence C. Paulson
2022-04-20: The Generalized Multiset Ordering is NP-Complete
Authors: René Thiemann and Lukas Schmidinger
+ 2022-04-10: The Sophomore's Dream +
+ Author: + Manuel Eberl +
2022-04-08: A Combinator Library for Prefix-Free Codes
Author: Emin Karayel
2022-04-08: Formalization of Randomized Approximation Algorithms for Frequency Moments
Author: Emin Karayel
2022-03-24: Constructing the Reals as Dedekind Cuts of Rationals
Authors: Jacques D. Fleuriot and Lawrence C. Paulson
2022-03-23: Ackermann's Function Is Not Primitive Recursive
Author: Lawrence C. Paulson
2022-03-22: A Naive Prover for First-Order Logic
Author: Asta Halkjær From
2022-03-15: A Proof from THE BOOK: The Partial Fraction Expansion of the Cotangent
Author: Manuel Eberl
2022-03-06: The Independence of the Continuum Hypothesis in Isabelle/ZF
Authors: Emmanuel Gunther, Miguel Pagano, Pedro Sánchez Terraf - and and Matías Steinberg + and Matías Steinberg
2022-03-03: Transitive Models of Fragments of ZFC
Authors: Emmanuel Gunther, Miguel Pagano, Pedro Sánchez Terraf - and and Matías Steinberg + and Matías Steinberg
2022-02-28: Residuated Transition Systems
Author: Eugene W. Stark
2022-02-20: Universal Hash Families
Author: Emin Karayel
2022-02-18: Wetzel's Problem and the Continuum Hypothesis
Author: Lawrence C Paulson
2022-02-15: First-Order Query Evaluation
Author: Martin Raszyk
2022-02-13: Multi-Head Monitoring of Metric Dynamic Logic
Author: Martin Raszyk
2022-02-04: Enumeration of Equivalence Relations
Author: Emin Karayel
2022-02-03: Quasi-Borel Spaces
Authors: Michikazu Hirata, Yasuhiko Minamide and Tetsuya Sato
2022-02-03: Duality of Linear Programming
Author: René Thiemann
2022-02-02: First-Order Theory of Rewriting
Authors: Alexander Lochmann and Bertram Felgenhauer
2022-01-31: Young's Inequality for Increasing Functions
Author: Lawrence C Paulson
2022-01-31: A Sequent Calculus Prover for First-Order Logic with Functions
Authors: Asta Halkjær From and Frederik Krogsdal Jacobsen
2022-01-29: Interpolation Polynomials (in HOL-Algebra)
Author: Emin Karayel
2022-01-25: Median Method
Author: Emin Karayel
2022-01-23: Actuarial Mathematics
Author: Yosuke Ito
2022-01-08: Irrational numbers from THE BOOK
Author: Lawrence C Paulson
2022-01-04: Knight's Tour Revisited Revisited
Author: Lukas Koller

 

2021
2021-12-31: Hyperdual Numbers and Forward Differentiation
Authors: Filip Smola and Jacques Fleuriot
2021-12-29: Gale-Shapley Algorithm
Author: Tobias Nipkow
2021-12-28: Roth's Theorem on Arithmetic Progressions
Authors: Chelsea Edmonds, Angeliki Koutsoukou-Argyraki and Lawrence C. Paulson
2021-12-16: Markov Decision Processes with Rewards
Authors: Maximilian Schäffeler and Mohammad Abdulaziz
2021-12-16: Verified Algorithms for Solving Markov Decision Processes
Authors: Maximilian Schäffeler and Mohammad Abdulaziz
2021-12-15: Regular Tree Relations
Authors: Alexander Lochmann, Bertram Felgenhauer, Christian Sternagel, René Thiemann and Thomas Sternagel
2021-11-29: Simplicial Complexes and Boolean functions
Authors: Jesús Aransay, Alejandro del Campo and Julius Michaelis
2021-11-23: van Emde Boas Trees
Authors: Thomas Ammer and Peter Lammich
2021-11-22: Foundation of geometry in planes, and some complements: Excluding the parallel axioms
Author: Fumiya Iwama
2021-11-19: The Hahn and Jordan Decomposition Theorems
Authors: Marie Cousin, Mnacho Echenim and Hervé Guiol
2021-11-08: Exploring Simplified Variants of Gödel’s Ontological Argument in Isabelle/HOL
Author: Christoph Benzmüller
2021-11-08: Real Exponents as the Limits of Sequences of Rational Exponents
Author: Jacques D. Fleuriot
2021-11-08: Automating Public Announcement Logic and the Wise Men Puzzle in Isabelle/HOL
Authors: Christoph Benzmüller and Sebastian Reiche
2021-11-08: Factorization of Polynomials with Algebraic Coefficients
Authors: Manuel Eberl and René Thiemann
2021-11-05: Szemerédi's Regularity Lemma
Authors: Chelsea Edmonds, Angeliki Koutsoukou-Argyraki and Lawrence C. Paulson
2021-10-28: Quantum and Classical Registers
Author: Dominique Unruh
2021-10-19: Belief Revision Theory
Authors: Valentin Fouillard, Safouan Taha, Frédéric Boulanger and Nicolas Sabouret
2021-10-13: X86 instruction semantics and basic block symbolic execution
Authors: Freek Verbeek, Abhijith Bharadwaj, Joshua Bockenek, Ian Roessle, Timmy Weerwag and Binoy Ravindran
2021-10-12: Algebras for Iteration, Infinite Executions and Correctness of Sequential Computations
Author: Walter Guttmann
2021-10-02: Verified Quadratic Virtual Substitution for Real Arithmetic
Authors: Matias Scharager, Katherine Cordwell, Stefan Mitsch and André Platzer
2021-09-24: Soundness and Completeness of an Axiomatic System for First-Order Logic
Author: Asta Halkjær From
2021-09-18: Complex Bounded Operators
Authors: Jose Manuel Rodriguez Caballero and Dominique Unruh
2021-09-16: A Formalization of Weighted Path Orders and Recursive Path Orders
Authors: Christian Sternagel, René Thiemann and Akihisa Yamada
2021-09-06: Extension of Types-To-Sets
Author: Mihails Milehins
2021-09-06: IDE: Introduction, Destruction, Elimination
Author: Mihails Milehins
2021-09-06: Conditional Transfer Rule
Author: Mihails Milehins
2021-09-06: Conditional Simplification
Author: Mihails Milehins
2021-09-06: Category Theory for ZFC in HOL III: Universal Constructions
Author: Mihails Milehins
2021-09-06: Category Theory for ZFC in HOL I: Foundations: Design Patterns, Set Theory, Digraphs, Semicategories
Author: Mihails Milehins
2021-09-06: Category Theory for ZFC in HOL II: Elementary Theory of 1-Categories
Author: Mihails Milehins
2021-09-05: A data flow analysis algorithm for computing dominators
Author: Nan Jiang
2021-09-03: Solving Cubic and Quartic Equations
Author: René Thiemann
2021-08-26: Logging-independent Message Anonymity in the Relational Method
Author: Pasquale Noce
2021-08-21: The Theorem of Three Circles
Authors: Fox Thomson and Wenda Li
2021-08-16: Fresh identifiers
Authors: Andrei Popescu and Thomas Bauereiss
2021-08-16: CoSMed: A confidentiality-verified social media platform
Authors: Thomas Bauereiss and Andrei Popescu
2021-08-16: CoSMeDis: A confidentiality-verified distributed social media platform
Authors: Thomas Bauereiss and Andrei Popescu
2021-08-16: CoCon: A Confidentiality-Verified Conference Management System
Authors: Andrei Popescu, Peter Lammich and Thomas Bauereiss
2021-08-16: Compositional BD Security
Authors: Thomas Bauereiss and Andrei Popescu
2021-08-13: Combinatorial Design Theory
Authors: Chelsea Edmonds and Lawrence Paulson
2021-08-03: Relational Forests
Author: Walter Guttmann
2021-07-27: Schutz' Independent Axioms for Minkowski Spacetime
Authors: Richard Schmoetten, Jake Palmer and Jacques Fleuriot
2021-07-07: Finitely Generated Abelian Groups
Authors: Joseph Thommes and Manuel Eberl
2021-07-01: SpecCheck - Specification-Based Testing for Isabelle/ML
Authors: Kevin Kappelmann, Lukas Bulwahn and Sebastian Willenbrink
2021-06-22: Van der Waerden's Theorem
Authors: Katharina Kreuzer and Manuel Eberl
2021-06-18: MiniSail - A kernel language for the ISA specification language SAIL
Author: Mark Wassell
2021-06-17: Public Announcement Logic
Author: Asta Halkjær From
2021-06-04: A Shorter Compiler Correctness Proof for Language IMP
Author: Pasquale Noce
2021-05-24: Lyndon words
Authors: Štěpán Holub and Štěpán Starosta
2021-05-24: Graph Lemma
Authors: Štěpán Holub and Štěpán Starosta
2021-05-24: Combinatorics on Words Basics
Authors: Štěpán Holub, Martin Raška and Štěpán Starosta
2021-04-30: Regression Test Selection
Author: Susannah Mansky
2021-04-27: Isabelle's Metalogic: Formalization and Proof Checker
Authors: Tobias Nipkow and Simon Roßkopf
2021-04-27: Lifting the Exponent
Author: Jakub Kądziołka
2021-04-24: The BKR Decision Procedure for Univariate Real Arithmetic
Authors: Katherine Cordwell, Yong Kiam Tan and André Platzer
2021-04-23: Gale-Stewart Games
Author: Sebastiaan Joosten
2021-04-13: Formalization of Timely Dataflow's Progress Tracking Protocol
Authors: Matthias Brun, Sára Decova, Andrea Lattuada and Dmitriy Traytel
2021-04-01: Information Flow Control via Dependency Tracking
Author: Benedikt Nordhoff
2021-03-29: Grothendieck's Schemes in Algebraic Geometry
Authors: Anthony Bordg, Lawrence Paulson and Wenda Li
2021-03-23: Hensel's Lemma for the p-adic Integers
Author: Aaron Crighton
2021-03-17: Constructive Cryptography in HOL: the Communication Modeling Aspect
Authors: Andreas Lochbihler and S. Reza Sefidgar
2021-03-12: Two algorithms based on modular arithmetic: lattice basis reduction and Hermite normal form computation
Authors: Ralph Bottesch, Jose Divasón and René 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, Simon Robillard and Ujkan Sulejmani
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: Rose 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: Order Extension and Szpilrajn's Extension Theorem
Authors: Peter Zeller and Lukas Stevens
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, 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, 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: Completeness of Modal Logics
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, 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: Rose 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, Peter Lammich and Thomas Bauereiss
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,680 +1,670 @@ 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. 08 May 2022 00:00:00 +0000 Clique is not solvable by monotone circuits of polynomial size https://www.isa-afp.org/entries/Clique_and_Monotone_Circuits.html https://www.isa-afp.org/entries/Clique_and_Monotone_Circuits.html René Thiemann 08 May 2022 00:00:00 +0000 <p> Given a graph $G$ with $n$ vertices and a number $s$, the decision problem Clique asks whether $G$ contains a fully connected subgraph with $s$ vertices. For this NP-complete problem there exists a non-trivial lower bound: no monotone circuit of a size that is polynomial in $n$ can solve Clique. </p><p> This entry provides an Isabelle/HOL formalization of a concrete lower bound (the bound is $\sqrt[7]{n}^{\sqrt[8]{n}}$ for the fixed choice of $s = \sqrt[4]{n}$), following a proof by Gordeev. </p> Fisher's Inequality: Linear Algebraic Proof Techniques for Combinatorics https://www.isa-afp.org/entries/Fishers_Inequality.html https://www.isa-afp.org/entries/Fishers_Inequality.html Chelsea Edmonds, Lawrence C. Paulson 21 Apr 2022 00:00:00 +0000 Linear algebraic techniques are powerful, yet often underrated tools in combinatorial proofs. This formalisation provides a library including matrix representations of incidence set systems, general formal proof techniques for the rank argument and linear bound argument, and finally a formalisation of a number of variations of the well-known Fisher's inequality. We build on our prior work formalising combinatorial design theory using a locale-centric approach, including extensions such as constant intersect designs and dual incidence systems. In addition to Fisher's inequality, we also formalise proofs on other incidence system properties using the incidence matrix representation, such as design existence, dual system relationships and incidence system isomorphisms. This formalisation is presented in the paper "Formalising Fisher's Inequality: Formal Linear Algebraic Techniques in Combinatorics", accepted to ITP 2022. The Generalized Multiset Ordering is NP-Complete https://www.isa-afp.org/entries/Multiset_Ordering_NPC.html https://www.isa-afp.org/entries/Multiset_Ordering_NPC.html René Thiemann, Lukas Schmidinger 20 Apr 2022 00:00:00 +0000 We consider the problem of comparing two multisets via the generalized multiset ordering. We show that the corresponding decision problem is NP-complete. To be more precise, we encode multiset-comparisons into propositional formulas or into conjunctive normal forms of quadratic size; we further prove that satisfiability of conjunctive normal forms can be encoded as multiset-comparison problems of linear size. As a corollary, we also show that the problem of deciding whether two terms are related by a recursive path order is NP-hard, provided the recursive path order is based on the generalized multiset ordering. + The Sophomore's Dream + https://www.isa-afp.org/entries/Sophomores_Dream.html + https://www.isa-afp.org/entries/Sophomores_Dream.html + Manuel Eberl + 10 Apr 2022 00:00:00 +0000 + +<p>This article provides a brief formalisation of the two +equations known as the <em>Sophomore's Dream</em>, +first discovered by Johann Bernoulli in 1697:</p> \[\int_0^1 +x^{-x}\,\text{d}x = \sum_{n=1}^\infty n^{-n} \quad\text{and}\quad +\int_0^1 x^x\,\text{d}x = -\sum_{n=1}^\infty (-n)^{-n}\] + + A Combinator Library for Prefix-Free Codes https://www.isa-afp.org/entries/Prefix_Free_Code_Combinators.html https://www.isa-afp.org/entries/Prefix_Free_Code_Combinators.html Emin Karayel 08 Apr 2022 00:00:00 +0000 This entry contains a set of binary encodings for primitive data types, such as natural numbers, integers, floating-point numbers as well as combinators to construct encodings for products, lists, sets or functions of/between such types. For natural numbers and integers, the entry contains various encodings, such as Elias-Gamma-Codes and exponential Golomb Codes, which are efficient variable-length codes in use by current compression formats. A use-case for this library is measuring the persisted size of a complex data structure without having to hand-craft a dedicated encoding for it, independent of Isabelle's internal representation. Formalization of Randomized Approximation Algorithms for Frequency Moments https://www.isa-afp.org/entries/Frequency_Moments.html https://www.isa-afp.org/entries/Frequency_Moments.html Emin Karayel 08 Apr 2022 00:00:00 +0000 In 1999 Alon et. al. introduced the still active research topic of approximating the frequency moments of a data stream using randomized algorithms with minimal space usage. This includes the problem of estimating the cardinality of the stream elements - the zeroth frequency moment. But, also higher-order frequency moments that provide information about the skew of the data stream. (The <i>k</i>-th frequency moment of a data stream is the sum of the <i>k</i>-th powers of the occurrence counts of each element in the stream.) This entry formalizes three randomized algorithms for the approximation of <i>F<sub>0</sub></i>, <i>F<sub>2</sub></i> and <i>F<sub>k</sub></i> for <i>k ≥ 3</i> based on [<a href="https://doi.org/10.1006/jcss.1997.1545">1</a>, <a href="https://doi.org/10.1007/3-540-45726-7_1">2</a>] and verifies their expected accuracy, success probability and space usage. Constructing the Reals as Dedekind Cuts of Rationals https://www.isa-afp.org/entries/Dedekind_Real.html https://www.isa-afp.org/entries/Dedekind_Real.html Jacques D. Fleuriot, Lawrence C. Paulson 24 Mar 2022 00:00:00 +0000 The type of real numbers is constructed from the positive rationals using the method of Dedekind cuts. This development, briefly described in papers by the authors, follows the textbook presentation by Gleason. It's notable that the first formalisation of a significant piece of mathematics, by Jutting in 1977, involved a similar construction. Ackermann's Function Is Not Primitive Recursive https://www.isa-afp.org/entries/Ackermanns_not_PR.html https://www.isa-afp.org/entries/Ackermanns_not_PR.html Lawrence C. Paulson 23 Mar 2022 00:00:00 +0000 Ackermann's function is defined in the usual way and a number of its elementary properties are proved. Then, the primitive recursive functions are defined inductively: as a predicate on the functions that map lists of numbers to numbers. It is shown that every primitive recursive function is strictly dominated by Ackermann's function. The formalisation follows an earlier one by Nora Szasz. A Naive Prover for First-Order Logic https://www.isa-afp.org/entries/FOL_Seq_Calc3.html https://www.isa-afp.org/entries/FOL_Seq_Calc3.html Asta Halkjær From 22 Mar 2022 00:00:00 +0000 <p> The AFP entry <a href="https://www.isa-afp.org/entries/Abstract_Completeness.html">Abstract Completeness</a> by Blanchette, Popescu and Traytel formalizes the core of Beth/Hintikka-style completeness proofs for first-order logic and can be used to formalize executable sequent calculus provers. In the Journal of Automated Reasoning, the authors instantiate the framework with a sequent calculus for first-order logic and prove its completeness. Their use of an infinite set of proof rules indexed by formulas yields very direct arguments. A fair stream of these rules controls the prover, making its definition remarkably simple. The AFP entry, however, only contains a toy example for propositional logic. The AFP entry <a href="https://www.isa-afp.org/entries/FOL_Seq_Calc2.html">A Sequent Calculus Prover for First-Order Logic with Functions</a> by From and Jacobsen also uses the framework, but uses a finite set of generic rules resulting in a more sophisticated prover with more complicated proofs. </p> <p> This entry contains an executable sequent calculus prover for first-order logic with functions in the style presented by Blanchette et al. The prover can be exported to Haskell and this entry includes formalized proofs of its soundness and completeness. The proofs are simpler than those for the prover by From and Jacobsen but the performance of the prover is significantly worse. </p> <p> The included theory <em>Fair-Stream</em> first proves that the sequence of natural numbers 0, 0, 1, 0, 1, 2, etc. is fair. It then proves that mapping any surjective function across the sequence preserves fairness. This method of obtaining a fair stream of rules is similar to the one given by Blanchette et al. The concrete functions from natural numbers to terms, formulas and rules are defined using the <em>Nat-Bijection</em> theory in the HOL-Library. </p> A Proof from THE BOOK: The Partial Fraction Expansion of the Cotangent https://www.isa-afp.org/entries/Cotangent_PFD_Formula.html https://www.isa-afp.org/entries/Cotangent_PFD_Formula.html Manuel Eberl 15 Mar 2022 00:00:00 +0000 <p>In this article, I formalise a proof from <a href="https://dx.doi.org/10.1007/978-3-662-57265-8">THE BOOK</a>; namely a formula that was called ‘one of the most beautiful formulas involving elementary functions’:</p> \[\pi \cot(\pi z) = \frac{1}{z} + \sum_{n=1}^\infty\left(\frac{1}{z+n} + \frac{1}{z-n}\right)\] <p>The proof uses Herglotz's trick to show the real case and analytic continuation for the complex case.</p> The Independence of the Continuum Hypothesis in Isabelle/ZF https://www.isa-afp.org/entries/Independence_CH.html https://www.isa-afp.org/entries/Independence_CH.html - Emmanuel Gunther, Miguel Pagano, Pedro Sánchez Terraf, and Matías Steinberg + Emmanuel Gunther, Miguel Pagano, Pedro Sánchez Terraf, Matías Steinberg 06 Mar 2022 00:00:00 +0000 We redeveloped our formalization of forcing in the set theory framework of Isabelle/ZF. Under the assumption of the existence of a countable transitive model of ZFC, we construct proper generic extensions that satisfy the Continuum Hypothesis and its negation. Transitive Models of Fragments of ZFC https://www.isa-afp.org/entries/Transitive_Models.html https://www.isa-afp.org/entries/Transitive_Models.html - Emmanuel Gunther, Miguel Pagano, Pedro Sánchez Terraf, and Matías Steinberg + Emmanuel Gunther, Miguel Pagano, Pedro Sánchez Terraf, Matías Steinberg 03 Mar 2022 00:00:00 +0000 We extend the ZF-Constructibility library by relativizing theories of the Isabelle/ZF and Delta System Lemma sessions to a transitive class. We also relativize Paulson's work on Aleph and our former treatment of the Axiom of Dependent Choices. This work is a prerrequisite to our formalization of the independence of the Continuum Hypothesis. Residuated Transition Systems https://www.isa-afp.org/entries/ResiduatedTransitionSystem.html https://www.isa-afp.org/entries/ResiduatedTransitionSystem.html Eugene W. Stark 28 Feb 2022 00:00:00 +0000 <p> A <em>residuated transition system</em> (RTS) is a transition system that is equipped with a certain partial binary operation, called <em>residuation</em>, on transitions. Using the residuation operation, one can express nuances, such as a distinction between nondeterministic and concurrent choice, as well as partial commutativity relationships between transitions, which are not captured by ordinary transition systems. A version of residuated transition systems was introduced in previous work by the author, in which they were called “concurrent transition systems” in view of the original motivation for their definition from the study of concurrency. In the first part of the present article, we give a formal development that generalizes and subsumes the original presentation. We give an axiomatic definition of residuated transition systems that assumes only a single partial binary operation as given structure. From the axioms, we derive notions of “arrow“ (transition), “source”, “target”, “identity”, as well as “composition” and “join” of transitions; thereby recovering structure that in the previous work was assumed as given. We formalize and generalize the result, that residuation extends from transitions to transition paths, and we systematically develop the properties of this extension. A significant generalization made in the present work is the identification of a general notion of congruence on RTS’s, along with an associated quotient construction. </p> <p> In the second part of this article, we use the RTS framework to formalize several results in the theory of reduction in Church’s λ-calculus. Using a de Bruijn index-based syntax in which terms represent parallel reduction steps, we define residuation on terms and show that it satisfies the axioms for an RTS. An application of the results on paths from the first part of the article allows us to prove the classical Church-Rosser Theorem with little additional effort. We then use residuation to define the notion of “development” and we prove the Finite Developments Theorem, that every development is finite, formalizing and adapting to de Bruijn indices a proof by de Vrijer. We also use residuation to define the notion of a “standard reduction path”, and we prove the Standardization Theorem: that every reduction path is congruent to a standard one. As a corollary of the Standardization Theorem, we obtain the Leftmost Reduction Theorem: that leftmost reduction is a normalizing strategy. </p> Universal Hash Families https://www.isa-afp.org/entries/Universal_Hash_Families.html https://www.isa-afp.org/entries/Universal_Hash_Families.html Emin Karayel 20 Feb 2022 00:00:00 +0000 A <i>k</i>-universal hash family is a probability space of functions, which have uniform distribution and form <i>k</i>-wise independent random variables. They can often be used in place of classic (or cryptographic) hash functions and allow the rigorous analysis of the performance of randomized algorithms and data structures that rely on hash functions. In 1981 <a href="https://doi.org/10.1016/0022-0000(81)90033-7">Wegman and Carter</a> introduced a generic construction for such families with arbitrary <i>k</i> using polynomials over a finite field. This entry contains a formalization of them and establishes the property of <i>k</i>-universality. To be useful the formalization also provides an explicit construction of finite fields using the factor ring of integers modulo a prime. Additionally, some generic results about independent families are shown that might be of independent interest. Wetzel's Problem and the Continuum Hypothesis https://www.isa-afp.org/entries/Wetzels_Problem.html https://www.isa-afp.org/entries/Wetzels_Problem.html Lawrence C Paulson 18 Feb 2022 00:00:00 +0000 Let $F$ be a set of analytic functions on the complex plane such that, for each $z\in\mathbb{C}$, the set $\{f(z) \mid f\in F\}$ is countable; must then $F$ itself be countable? The answer is yes if the Continuum Hypothesis is false, i.e., if the cardinality of $\mathbb{R}$ exceeds $\aleph_1$. But if CH is true then such an $F$, of cardinality $\aleph_1$, can be constructed by transfinite recursion. The formal proof illustrates reasoning about complex analysis (analytic and homomorphic functions) and set theory (transfinite cardinalities) in a single setting. The mathematical text comes from <em>Proofs from THE BOOK</em> by Aigner and Ziegler. First-Order Query Evaluation https://www.isa-afp.org/entries/Eval_FO.html https://www.isa-afp.org/entries/Eval_FO.html Martin Raszyk 15 Feb 2022 00:00:00 +0000 We formalize first-order query evaluation over an infinite domain with equality. We first define the syntax and semantics of first-order logic with equality. Next we define a locale <i>eval&lowbar;fo</i> abstracting a representation of a potentially infinite set of tuples satisfying a first-order query over finite relations. Inside the locale, we define a function <i>eval</i> checking if the set of tuples satisfying a first-order query over a database (an interpretation of the query's predicates) is finite (i.e., deciding <i>relative safety</i>) and computing the set of satisfying tuples if it is finite. Altogether the function <i>eval</i> solves <i>capturability</i> (Avron and Hirshfeld, 1991) of first-order logic with equality. We also use the function <i>eval</i> to prove a code equation for the semantics of first-order logic, i.e., the function checking if a first-order query over a database is satisfied by a variable assignment.<br/> We provide an interpretation of the locale <i>eval&lowbar;fo</i> based on the approach by Ailamazyan et al. A core notion in the interpretation is the active domain of a query and a database that contains all domain elements that occur in the database or interpret the query's constants. We prove the main theorem of Ailamazyan et al. relating the satisfaction of a first-order query over an infinite domain to the satisfaction of this query over a finite domain consisting of the active domain and a few additional domain elements (outside the active domain) whose number only depends on the query. In our interpretation of the locale <i>eval&lowbar;fo</i>, we use a potentially higher number of the additional domain elements, but their number still only depends on the query and thus has no effect on the data complexity (Vardi, 1982) of query evaluation. Our interpretation yields an <i>executable</i> function <i>eval</i>. The time complexity of <i>eval</i> on a query is linear in the total number of tuples in the intermediate relations for the subqueries. Specifically, we build a database index to evaluate a conjunction. We also optimize the case of a negated subquery in a conjunction. Finally, we export code for the infinite domain of natural numbers. Multi-Head Monitoring of Metric Dynamic Logic https://www.isa-afp.org/entries/VYDRA_MDL.html https://www.isa-afp.org/entries/VYDRA_MDL.html Martin Raszyk 13 Feb 2022 00:00:00 +0000 Runtime monitoring (or runtime verification) is an approach to checking compliance of a system's execution with a specification (e.g., a temporal query). The system's execution is logged into a trace---a sequence of time-points, each consisting of a time-stamp and observed events. A monitor is an algorithm that produces verdicts on the satisfaction of a temporal query on a trace. We formalize a monitoring algorithm for metric dynamic logic, an extension of metric temporal logic with regular expressions. The monitor computes whether a given query is satisfied at every position in an input trace of time-stamped events. We formalize the time-stamps as an abstract algebraic structure satisfying certain assumptions. Instances of this structure include natural numbers, real numbers, and lexicographic combinations of them. Our monitor follows the multi-head paradigm: it reads the input simultaneously at multiple positions and moves its reading heads asynchronously. This mode of operation results in unprecedented time and space complexity guarantees for metric dynamic logic: The monitor's amortized time complexity to process a time-point and the monitor's space complexity neither depends on the event-rate, i.e., the number of events within a fixed time-unit, nor on the numeric constants occurring in the quantitative temporal constraints in the given query. The multi-head monitoring algorithm for metric dynamic logic is reported in our paper "Multi-Head Monitoring of Metric Dynamic Logic" published at ATVA 2020. We have also formalized unpublished specialized algorithms for the temporal operators of metric temporal logic. Enumeration of Equivalence Relations https://www.isa-afp.org/entries/Equivalence_Relation_Enumeration.html https://www.isa-afp.org/entries/Equivalence_Relation_Enumeration.html Emin Karayel 04 Feb 2022 00:00:00 +0000 <p>This entry contains a formalization of an algorithm enumerating all equivalence relations on an initial segment of the natural numbers. The approach follows the method described by Stanton and White <a href="https://doi.org/10.1007/978-1-4612-4968-9">[5,§ 1.5]</a> using restricted growth functions.</p> <p>The algorithm internally enumerates restricted growth functions (as lists), whose equivalence kernels then form the equivalence relations. This has the advantage that the representation is compact and lookup of the relation reduces to a list lookup operation.</p> <p>The algorithm can also be used within a proof and an example application is included, where a sequence of variables is split by the possible partitions they can form.</p> Quasi-Borel Spaces https://www.isa-afp.org/entries/Quasi_Borel_Spaces.html https://www.isa-afp.org/entries/Quasi_Borel_Spaces.html Michikazu Hirata, Yasuhiko Minamide, Tetsuya Sato 03 Feb 2022 00:00:00 +0000 The notion of quasi-Borel spaces was introduced by <a href="https://dl.acm.org/doi/10.5555/3329995.3330072"> Heunen et al</a>. The theory provides a suitable denotational model for higher-order probabilistic programming languages with continuous distributions. This entry is a formalization of the theory of quasi-Borel spaces, including construction of quasi-Borel spaces (product, coproduct, function spaces), the adjunction between the category of measurable spaces and the category of quasi-Borel spaces, and the probability monad on quasi-Borel spaces. This entry also contains the formalization of the Bayesian regression presented in the work of Heunen et al. This work is a part of the work by same authors, <i>Program Logic for Higher-Order Probabilistic Programs in Isabelle/HOL</i>, which will be published in the proceedings of the 16th International Symposium on Functional and Logic Programming (FLOPS 2022). Duality of Linear Programming https://www.isa-afp.org/entries/LP_Duality.html https://www.isa-afp.org/entries/LP_Duality.html René Thiemann 03 Feb 2022 00:00:00 +0000 We formalize the weak and strong duality theorems of linear programming. For the strong duality theorem we provide three sufficient preconditions: both the primal problem and the dual problem are satisfiable, the primal problem is satisfiable and bounded, or the dual problem is satisfiable and bounded. The proofs are based on an existing formalization of Farkas' Lemma. First-Order Theory of Rewriting https://www.isa-afp.org/entries/FO_Theory_Rewriting.html https://www.isa-afp.org/entries/FO_Theory_Rewriting.html Alexander Lochmann, Bertram Felgenhauer 02 Feb 2022 00:00:00 +0000 The first-order theory of rewriting (FORT) is a decidable theory for linear variable-separated rewrite systems. The decision procedure is based on tree automata technique and an inference system presented in "Certifying Proofs in the First-Order Theory of Rewriting". This AFP entry provides a formalization of the underlying decision procedure. Moreover it allows to generate a function that can verify each inference step via the code generation facility of Isabelle/HOL. Additionally it contains the specification of a certificate language (that allows to state proofs in FORT) and a formalized function that allows to verify the validity of the proof. This gives software tool authors, that implement the decision procedure, the possibility to verify their output. Young's Inequality for Increasing Functions https://www.isa-afp.org/entries/Youngs_Inequality.html https://www.isa-afp.org/entries/Youngs_Inequality.html Lawrence C Paulson 31 Jan 2022 00:00:00 +0000 Young's inequality states that $$ ab \leq \int_0^a f(x)dx + \int_0^b f^{-1}(y) dy $$ where $a\geq 0$, $b\geq 0$ and $f$ is strictly increasing and continuous. Its proof is formalised following <a href="https://www.jstor.org/stable/2318018">the development</a> by Cunningham and Grossman. Their idea is to make the intuitive, geometric folklore proof rigorous by reasoning about step functions. The lack of the Riemann integral makes the development longer than one would like, but their argument is reproduced faithfully. A Sequent Calculus Prover for First-Order Logic with Functions https://www.isa-afp.org/entries/FOL_Seq_Calc2.html https://www.isa-afp.org/entries/FOL_Seq_Calc2.html Asta Halkjær From, Frederik Krogsdal Jacobsen 31 Jan 2022 00:00:00 +0000 We formalize an automated theorem prover for first-order logic with functions. The proof search procedure is based on sequent calculus and we verify its soundness and completeness using the Abstract Soundness and Abstract Completeness theories. Our analytic completeness proof covers both open and closed formulas. Since our deterministic prover considers only the subset of terms relevant to proving a given sequent, we do so as well when building a countermodel from a failed proof. We formally connect our prover with the proof system and semantics of the existing SeCaV system. In particular, the prover's output can be post-processed in Haskell to generate human-readable SeCaV proofs which are also machine-verifiable proof certificates. Interpolation Polynomials (in HOL-Algebra) https://www.isa-afp.org/entries/Interpolation_Polynomials_HOL_Algebra.html https://www.isa-afp.org/entries/Interpolation_Polynomials_HOL_Algebra.html Emin Karayel 29 Jan 2022 00:00:00 +0000 <p>A well known result from algebra is that, on any field, there is exactly one polynomial of degree less than n interpolating n points [<a href="https://doi.org/10.1017/CBO9780511814549">1</a>, §7].</p> <p>This entry contains a formalization of the above result, as well as the following generalization in the case of finite fields <i>F</i>: There are <i>|F|<sup>m-n</sup></i> polynomials of degree less than <i>m ≥ n</i> interpolating the same n points, where <i>|F|</i> denotes the size of the domain of the field. To establish the result the entry also includes a formalization of Lagrange interpolation, which might be of independent interest.</p> <p>The formalized results are defined on the algebraic structures from HOL-Algebra, which are distinct from the type-class based structures defined in HOL. Note that there is an existing formalization for polynomial interpolation and, in particular, Lagrange interpolation by Thiemann and Yamada [<a href="https://www.isa-afp.org/entries/Polynomial_Interpolation.html">2</a>] on the type-class based structures in HOL.</p> Median Method https://www.isa-afp.org/entries/Median_Method.html https://www.isa-afp.org/entries/Median_Method.html Emin Karayel 25 Jan 2022 00:00:00 +0000 <p>The median method is an amplification result for randomized approximation algorithms described in [<a href="https://doi.org/10.1006/jcss.1997.1545">1</a>]. Given an algorithm whose result is in a desired interval with a probability larger than <i>1/2</i>, it is possible to improve the success probability, by running the algorithm multiple times independently and using the median. In contrast to using the mean, the amplification of the success probability grows exponentially with the number of independent runs.</p> <p>This entry contains a formalization of the underlying theorem: Given a sequence of n independent random variables, which are in a desired interval with a probability <i>1/2 + a</i>. Then their median will be in the desired interval with a probability of <i>1 − exp(−2a<sup>2</sup> n)</i>. In particular, the success probability approaches <i>1</i> exponentially with the number of variables.</p> <p>In addition to that, this entry also contains a proof that order-statistics of Borel-measurable random variables are themselves measurable and that generalized intervals in linearly ordered Borel-spaces are measurable.</p> Actuarial Mathematics https://www.isa-afp.org/entries/Actuarial_Mathematics.html https://www.isa-afp.org/entries/Actuarial_Mathematics.html Yosuke Ito 23 Jan 2022 00:00:00 +0000 Actuarial Mathematics is a theory in applied mathematics, which is mainly used for determining the prices of insurance products and evaluating the liability of a company associating with insurance contracts. It is related to calculus, probability theory and financial theory, etc. In this entry, I formalize the very basic part of Actuarial Mathematics in Isabelle/HOL. The first formalization is about the theory of interest which deals with interest rates, present value factors, an annuity certain, etc. I have already formalized the basic part of Actuarial Mathematics in Coq (https://github.com/Yosuke-Ito-345/Actuary). This entry is currently the partial translation and a little generalization of the Coq formalization. The further translation in Isabelle/HOL is now proceeding. Irrational numbers from THE BOOK https://www.isa-afp.org/entries/Irrationals_From_THEBOOK.html https://www.isa-afp.org/entries/Irrationals_From_THEBOOK.html Lawrence C Paulson 08 Jan 2022 00:00:00 +0000 An elementary proof is formalised: that <em>exp r</em> is irrational for every nonzero rational number <em>r</em>. The mathematical development comes from the well-known volume <em>Proofs from THE BOOK</em>, by Aigner and Ziegler, who credit the idea to Hermite. The development illustrates a number of basic Isabelle techniques: the manipulation of summations, the calculation of quite complicated derivatives and the estimation of integrals. We also see how to import another AFP entry (Stirling's formula). As for the theorem itself, note that a much stronger and more general result (the Hermite--Lindemann--Weierstraß transcendence theorem) is already available in the AFP. Knight's Tour Revisited Revisited https://www.isa-afp.org/entries/Knights_Tour.html https://www.isa-afp.org/entries/Knights_Tour.html Lukas Koller 04 Jan 2022 00:00:00 +0000 This is a formalization of the article <i>Knight's Tour Revisited</i> by Cull and De Curtins where they prove the existence of a Knight's path for arbitrary <i>n &times; m</i>-boards with <i>min(n,m) &ge; 5</i>. If <i>n &middot; m</i> is even, then there exists a Knight's circuit. A Knight's Path is a sequence of moves of a Knight on a chessboard s.t. the Knight visits every square of a chessboard exactly once. Finding a Knight's path is a an instance of the Hamiltonian path problem. A Knight's circuit is a Knight's path, where additionally the Knight can move from the last square to the first square of the path, forming a loop. During the formalization two mistakes in the original proof were discovered. These mistakes are corrected in this formalization. Hyperdual Numbers and Forward Differentiation https://www.isa-afp.org/entries/Hyperdual.html https://www.isa-afp.org/entries/Hyperdual.html Filip Smola, Jacques Fleuriot 31 Dec 2021 00:00:00 +0000 <p>Hyperdual numbers are ones with a real component and a number of infinitesimal components, usually written as $a_0 + a_1 \cdot \epsilon_1 + a_2 \cdot \epsilon_2 + a_3 \cdot \epsilon_1\epsilon_2$. They have been proposed by <a href="https://doi.org/10.2514/6.2011-886">Fike and Alonso</a> in an approach to automatic differentiation.</p> <p>In this entry we formalise hyperdual numbers and their application to forward differentiation. We show them to be an instance of multiple algebraic structures and then, along with facts about twice-differentiability, we define what we call the hyperdual extensions of functions on real-normed fields. This extension formally represents the proposed way that the first and second derivatives of a function can be automatically calculated. We demonstrate it on the standard logistic function $f(x) = \frac{1}{1 + e^{-x}}$ and also reproduce the example analytic function $f(x) = \frac{e^x}{\sqrt{sin(x)^3 + cos(x)^3}}$ used for demonstration by Fike and Alonso.</p> Gale-Shapley Algorithm https://www.isa-afp.org/entries/Gale_Shapley.html https://www.isa-afp.org/entries/Gale_Shapley.html Tobias Nipkow 29 Dec 2021 00:00:00 +0000 This is a stepwise refinement and proof of the Gale-Shapley stable matching (or marriage) algorithm down to executable code. Both a purely functional implementation based on lists and a functional implementation based on efficient arrays (provided by the Collections Framework in the AFP) are developed. The latter implementation runs in time <i>O(n<sup>2</sup>)</i> where <i>n</i> is the cardinality of the two sets to be matched. - - Roth's Theorem on Arithmetic Progressions - https://www.isa-afp.org/entries/Roth_Arithmetic_Progressions.html - https://www.isa-afp.org/entries/Roth_Arithmetic_Progressions.html - Chelsea Edmonds, Angeliki Koutsoukou-Argyraki, Lawrence C. Paulson - 28 Dec 2021 00:00:00 +0000 - -We formalise a proof of Roth's Theorem on Arithmetic -Progressions, a major result in additive combinatorics on the -existence of 3-term arithmetic progressions in subsets of natural -numbers. To this end, we follow a proof using graph regularity. We -employ our recent formalisation of Szemerédi's Regularity Lemma, -a major result in extremal graph theory, which we use here to prove -the Triangle Counting Lemma and the Triangle Removal Lemma. Our -sources are Yufei Zhao's MIT lecture notes -"<a href="https://ocw.mit.edu/courses/mathematics/18-217-graph-theory-and-additive-combinatorics-fall-2019/lecture-notes/MIT18_217F19_ch3.pdf">Graph Theory and Additive Combinatorics</a>" -(revised version <a href="https://yufeizhao.com/gtac/gtac17.pdf">here</a>) -and W.T. Gowers's Cambridge lecture notes -"<a href="https://www.dpmms.cam.ac.uk/~par31/notes/tic.pdf">Topics in Combinatorics</a>". -We also refer to the University of -Georgia notes by Stephanie Bell and Will Grodzicki, -"<a href="http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.432.327">Using Szemerédi's Regularity Lemma to Prove Roth's Theorem</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:677
Number of Articles:678
Number of Authors:425
Number of lemmas:~197,100
Lines of Code:~3,405,600
Lines of Code:~3,406,100

Most used AFP articles:

NameUsed by ? articles
1. List-Index 21
2. Collections 14
Show 14
3. Coinductive 12
Jordan_Normal_Form 12
Polynomial_Factorization 12
Regular-Sets 12
4. Landau_Symbols 11
5. Abstract-Rewriting 10
Automatic_Refinement 10
Deriving 10

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,1067 +1,1068 @@ 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   Combinatorics_Words   Combinatorics_Words_Lyndon   Combinatorics_Words_Graph_Lemma   Regular_Tree_Relations   FO_Theory_Rewriting   ResiduatedTransitionSystem  

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   MDP-Algorithms   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   Regression_Test_Selection   Gale_Shapley   VYDRA_MDL   Universal_Hash_Families   Prefix_Free_Code_Combinators   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   Progress_Tracking   Concurrent: ConcurrentGC   Online: List_Update   Geometry: Closest_Pair_Points   Approximation: Approximation_Algorithms   Frequency_Moments   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   BenOr_Kozen_Reif   Smith_Normal_Form   Safe_Distance   Modular_arithmetic_LLL_and_HNF_algorithms   Virtual_Substitution   Equivalence_Relation_Enumeration   Optimization: Simplex   Quantum computing: Isabelle_Marries_Dirac   Projective_Measurements   Registers  

Concurrency

FLP   Concurrent_Ref_Alg   Concurrent_Revisions   Store_Buffer_Reduction   TESL_Language   ResiduatedTransitionSystem   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   Fresh_Identifiers   Van_Emde_Boas_Trees   Prefix_Free_Code_Combinators  

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   X86_Semantics  

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   ResiduatedTransitionSystem   Type systems: Name_Carrying_Type_Inference   MiniML   Possibilistic_Noninterference   SIFUM_Type_Systems   Dependent_SIFUM_Type_Systems   Strong_Security   WHATandWHERE_Security   VolpanoSmith   Physical_Quantities   MiniSail   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   Correctness_Algebras   Registers   Compiling: CakeML_Codegen   Compiling-Exceptions-Correctly   NormByEval   Density_Compiler   VeriComp   IMP_Compiler   Static analysis: RIPEMD-160-SPARK   Program-Conflict-Analysis   Shivers-CFA   Slicing   HRB-Slicing   InfPathElimination   Abs_Int_ITP2012   Dominance_CHK   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   IFC_Tracking   CoCon   BD_Security_Compositional   CoSMed   CoSMeDis   Logging_Independent_Anonymity   Cryptography: Game_Based_Crypto   Sigma_Commit_Crypto   CryptHOL   Constructive_Cryptography   RSAPSS   Elliptic_Curves_Group_Law   Constructive_Cryptography_CM  

Semantics

Launchbury   Clean   Transformer_Semantics   HOL-CSP   QHLProver   TESL_Language   Isabelle_C   CSP_RefTK   X86_Semantics   Registers   Quasi_Borel_Spaces  

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   SimplifiedOntologicalArgument  

General logic

Topological_Semantics   Metalogic_ProofChecker   Classical propositional logic: Free-Boolean-Algebra   Classical first-order logic: FOL-Fitting   FOL_Seq_Calc2   FOL_Axiomatic   Eval_FO   FOL_Seq_Calc3   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   FOL_Seq_Calc2   Saturation_Framework   Saturation_Framework_Extensions   FOL_Seq_Calc3   Lambda calculus: LambdaMu   Logics of knowledge and belief: Epistemic_Logic   Blue_Eyes   Public_Announcement_Logic   Belief_Revision   PAL   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   SimplifiedOntologicalArgument   Paraconsistent logics: Paraconsistency  

Computability

Universal_Turing_Machine   Recursion-Theory-I   Inductive_Inference   Minsky_Machines   Ackermanns_not_PR  

Set theory

Ordinal   Ordinals_and_Cardinals   HereditarilyFinite   ZFC_in_HOL   Forcing   Delta_System_Lemma   Transitive_Models   Independence_CH   Recursion-Addition   Ordinal_Partitions   CZH_Foundations   Wetzels_Problem  

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   FOL_Seq_Calc2   FOL_Axiomatic   FO_Theory_Rewriting   FOL_Seq_Calc3  

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   Weighted_Path_Order   FO_Theory_Rewriting   Multiset_Ordering_NPC  

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   Finitely_Generated_Abelian_Groups   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   Grothendieck_Schemes   Factor_Algebraic_Polynomial   Hyperdual   Interpolation_Polynomials_HOL_Algebra   LP_Duality   Fishers_Inequality  

Analysis

Banach_Steinhaus   Fourier   + Sophomores_Dream   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   Cubic_Quartic_Equations   Real_Power   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   Cotangent_PFD_Formula   Three_Circles   Complex_Bounded_Operators   Hyperdual   Youngs_Inequality   Wetzels_Problem   Dedekind_Real  

Measure theory

Hahn_Jordan_Decomposition  

Probability theory

DiscretePricing   CryptHOL   Constructive_Cryptography   Probabilistic_While   Markov_Models   MDP-Rewards   MDP-Algorithms   Density_Compiler   Probabilistic_Timed_Automata   Hidden_Markov_Models   Random_Graph_Subgraph_Threshold   Ergodic_Theory   Source_Coding_Theorem   Buffons_Needle   Laws_of_Large_Numbers   Constructive_Cryptography_CM   Median_Method   Universal_Hash_Families   Frequency_Moments  

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   Padic_Ints   Lifting_the_Exponent   Irrationals_From_THEBOOK  

Games and economics

DiscretePricing   ArrowImpossibilityGS   SenSocialChoice   Vickrey_Clarke_Groves   Actuarial_Mathematics   Parity_Game   First_Welfare_Theorem   Randomised_Social_Choice   SDS_Impossibility   Stable_Matching   Fishburn_Impossibility   Neumann_Morgenstern_Utility   GaleStewart_Games   Gale_Shapley  

Geometry

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

Topology

Topology   Knot_Theory   Kuratowski_Closure_Complement   Smooth_Manifolds   Simplicial_complexes_and_boolean_functions  

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   Relational_Forests   Szemeredi_Regularity   Roth_Arithmetic_Progressions   Knights_Tour  

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   Van_der_Waerden   Latin_Square   Bell_Numbers_Spivey   Catalan_Numbers   Falling_Factorial_Sum   Matroids   Delta_System_Lemma   Nash_Williams   Ordinal_Partitions   Sunflowers   Design_Theory   Szemeredi_Regularity   Roth_Arithmetic_Progressions   Equivalence_Relation_Enumeration   Fishers_Inequality   Clique_and_Monotone_Circuits  

Category theory

Category3   MonoidalCategory   Category   Category2   AxiomaticCategoryTheory   Bicategory   CZH_Foundations   CZH_Elementary_Categories   CZH_Universal_Constructions  

Physics

No_FTL_observers   Schutz_Spacetime   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   SpecCheck   Conditional_Simplification   Intro_Dest_Elim   Conditional_Transfer_Rule   Types_To_Sets_Extension  
\ No newline at end of file