Dependencies

2024

Word_Lib

May 10

Universal_Hash_Families

May 10

Root_Balanced_Tree

May 10

Number_Theoretic_Transform

May 10

Karatsuba

May 10

Akra_Bazzi

May 10

Prime_Number_Theorem

May 05

Show

May 02

Regular-Sets

Apr 26

Poincare_Bendixson

Apr 26

Functional-Automata

Apr 26

Well_Quasi_Orders

Apr 25

Polynomials

Apr 25

Lambda_Free_RPOs

Apr 25

Knuth_Bendix_Order

Apr 25

First_Order_Terms

Apr 25

Factor_Algebraic_Polynomial

Apr 25

Optics

Apr 16

MFOTL_Monitor

Apr 16

Coinductive

Apr 16

Psi_Calculi

Mar 27

QHLProver

Mar 26

Undirected_Graph_Theory

Mar 24

Distributed_Distinct_Elements

Mar 24

Zeta_Function

Mar 20

Polynomial_Factorization

Mar 20

Pell

Mar 20

Monad_Normalisation

Mar 15

Frequency_Moments

Mar 15

Concentration_Inequalities

Mar 15

Three_Squares

Mar 06

Expander_Graphs

Feb 19

Martingales

Feb 15

Catoids

Jan 24

2023

HOL-CSPM

Dec 24

Game_Based_Crypto

Dec 18

CRYSTALS-Kyber

Dec 18

CryptHOL

Dec 18

HOL-CSP

Dec 05

Collections

Nov 27

Polylog

Nov 24

Dirichlet_Series

Nov 24

ZFC_in_HOL

Nov 20

Linear_Recurrences

Nov 15

Formal_Puiseux_Series

Nov 14

Polynomial_Interpolation

Nov 13

Lp

Nov 13

Descartes_Sign_Rule

Nov 13

Perfect_Fields

Nov 06

Mason_Stothers

Nov 06

Berlekamp_Zassenhaus

Nov 06

Finite-Map-Extras

Nov 04

Standard_Borel_Spaces

Nov 02

S_Finite_Measure_Monad

Nov 02

Labeled_Transition_Systems

Oct 31

Deriving

Oct 31

ML_Unification

Oct 11

Twelvefold_Way

Sep 23

Lovasz_Local

Sep 23

Hypergraph_Basics

Sep 23

Girth_Chromatic

Sep 23

Card_Partitions

Sep 23

Stone_Relation_Algebras

Sep 22

List-Infinite

Sep 22

Fishers_Inequality

Sep 20

Design_Theory

Sep 20

SpecCheck

Sep 19

Triangle

Aug 16

Relation_Algebra

Aug 14

Quantales_Converse

Aug 14

Quantales

Aug 14

KAD

Aug 14

Kleene_Algebra

Jul 25

Probabilistic_While

Jun 19

Elliptic_Curves_Group_Law

Jun 06

Weighted_Path_Order

Jun 01

Complete_Non_Orders

May 24

List-Index

May 05

HereditarilyFinite

May 05

Graph_Theory

May 05

Fresh_Identifiers

May 05

Dirichlet_L

May 03

Skip_Lists

Apr 27

Jordan_Normal_Form

Apr 27

Saturation_Framework_Extensions

Apr 20

Saturation_Framework

Apr 20

Ordered_Resolution_Prover

Apr 20

Functional_Ordered_Resolution_Prover

Apr 20

Commuting_Hermitian

Apr 18

Stirling_Formula

Apr 03

Discrete_Summation

Apr 03

Weighted_Arithmetic_Geometric_Mean

Mar 03

Perron_Frobenius

Mar 03

Suppes_Theorem

Feb 20

LLL_Basis_Reduction

Feb 02

BenOr_Kozen_Reif

Feb 02

Propositional_Logic_Class

Jan 22

Combinatorics_Words_Graph_Lemma

Jan 03

Combinatorics_Words

Jan 03

2022

Virtual_Substitution

Dec 15

Datatype_Order_Generator

Dec 15

Algebraic_Numbers

Dec 15

Separation_Algebra

Nov 25

Containers

Nov 25

Pluennecke_Ruzsa_Inequality

Nov 21

Jacobson_Basic_Algebra

Nov 21

Random_Graph_Subgraph_Threshold

Nov 14

Falling_Factorial_Sum

Nov 11

Card_Number_Partitions

Nov 11

Randomised_Social_Choice

Nov 10

Epistemic_Logic

Sep 23

Padic_Ints

Sep 22

Localization_Ring

Sep 22

Bernoulli

Sep 02

Native_Word

Aug 09

Projective_Measurements

Jul 18

Lucas_Theorem

Jun 06

Digit_Expansions

Jun 06

Regular_Tree_Relations

Jun 02

Package_logic

May 30

Sunflowers

May 08

Groebner_Bases

Apr 21

Prefix_Free_Code_Combinators

Apr 08

Median_Method

Apr 08

Interpolation_Polynomials_HOL_Algebra

Apr 08

Equivalence_Relation_Enumeration

Apr 08

Bertrands_Postulate

Apr 08

Abstract_Soundness

Mar 22

Abstract_Completeness

Mar 22

Transitive_Models

Mar 06

Delta_System_Lemma

Mar 03

Finite_Fields

Feb 20

Card_Equiv_Relations

Feb 04

Linear_Inequalities

Feb 03

FOL-Fitting

Feb 02

FOL_Seq_Calc1

Jan 31

2021

Szemeredi_Regularity

Dec 28

Ergodic_Theory

Dec 28

MDP-Rewards

Dec 16

Gauss_Jordan

Dec 16

ROBDD

Nov 29

Refine_Imperative_HOL

Nov 29

Automatic_Refinement

Nov 23

Hermite_Lindemann

Nov 08

Complex_Bounded_Operators

Oct 28

Subset_Boolean_Algebras

Oct 12

Stone_Kleene_Relation_Algebras

Oct 12

MonoBoolTranAlgebra

Oct 12

Real_Impl

Sep 18

Banach_Steinhaus

Sep 18

Intro_Dest_Elim

Sep 06

CZH_Foundations

Sep 06

CZH_Elementary_Categories

Sep 06

Conditional_Transfer_Rule

Sep 06

Conditional_Simplification

Sep 06

Jinja

Sep 05

Complex_Geometry

Sep 03

Budan_Fourier

Aug 21

Bounded_Deducibility_Security

Aug 16

BD_Security_Compositional

Aug 16

Nested_Multisets_Ordinals

Aug 13

Nominal2

Jun 18

Szpilrajn

May 24

JinjaDCI

Apr 30

Sturm_Tarski

Apr 24

Parity_Game

Apr 23

Sigma_Commit_Crypto

Mar 17

Constructive_Cryptography

Mar 17

Smith_Normal_Form

Mar 12

Hermite

Mar 12

Power_Sum_Polynomials

Mar 03

Pi_Transcendental

Mar 03

Isabelle_Marries_Dirac

Mar 03

2020

Relational_Disjoint_Set_Forests

Dec 08

VeriComp

Dec 07

VectorSpace

Nov 22

Matrix_Tensor

Nov 22

Propositional_Proof_Systems

Oct 29

Certification_Monads

Oct 29

AI_Planning_Languages_Semantics

Oct 29

Shadow_SC_DOM

Sep 28

Shadow_DOM

Sep 28

Core_SC_DOM

Sep 28

Core_DOM

Sep 28

Syntax_Independent_Logic

Sep 16

Incompleteness

Sep 16

Goedel_Incompleteness

Sep 16

FinFun

Sep 07

Extended_Finite_State_Machines

Sep 07

Aggregation_Algebras

Aug 26

HOLCF-Prelude

Aug 25

Pratt_Certificate

Aug 04

Nash_Williams

Aug 03

Sturm_Sequences

Jun 01

Matrix

May 13

Prime_Distribution_Elementary

May 12

LTL_Master_Theorem

May 08

LTL

May 08

Symmetric_Polynomials

Apr 24

Hybrid_Systems_VCs

Apr 19

IEEE_Floating_Point

Apr 09

Generic_Join

Apr 09

Stateful_Protocol_Composition_and_Typing

Apr 08

Stone_Algebras

Jan 31

Probabilistic_Prime_Tests

Jan 17

MonoidalCategory

Jan 06

2019

E_Transcendental

Dec 27

Ordinary_Differential_Equations

Dec 18

Transformer_Semantics

Sep 10

KAT_and_DRA

Sep 10

Transition_Systems_and_Automata

Aug 16

Farkas

Aug 06

Pairing_Heap

Jul 08

Huffman

Jul 08

Higher_Order_Terms

Jul 08

Dict_Construction

Jul 08

Constructor_Funs

Jul 08

CakeML

Jul 08

Priority_Search_Trees

Jun 25

IMP2

Jun 13

Median_Of_Medians_Selection

May 30

Deep_Learning

Mar 24

Refine_Monadic

Feb 14

Matroids

Feb 14

Simplex

Jan 17

2018

Auto2_HOL

Dec 21

Order_Lattice_Props

Dec 11

Open_Induction

Nov 23

Random_BSTs

Oct 19

Recursion-Theory-I

Aug 14

Abstract-Rewriting

Aug 14

First_Welfare_Theorem

Jul 04

Stuttering_Equivalence

Jun 05

Monad_Memo_DP

May 27

Markov_Models

May 25

Timed_Automata

May 24

DynamicArchitectures

Mar 01

Landau_Symbols

Feb 06

Comparison_Sort_Lower_Bound

Feb 06

Affine_Arithmetic

Jan 08

2017

Finitely_Generated_Abelian_Groups

Dec 21

CRDT

Nov 09

Gabow_SCC

Oct 19

DFS_Framework

Oct 19

Winding_Number_Eval

Oct 17

Euler_MacLaurin

Oct 12

Count_Complex_Roots

Oct 12

Amortized_Complexity

Aug 20

Program-Conflict-Analysis

Jun 01

Flow_Networks

Jun 01

CAVA_Automata

Jun 01

Lazy_Case

May 24

Monomorphic_Monad

May 05

MFMC_Countable

May 05

Applicative_Lifting

May 05

Category3

May 04

Quick_Sort_Cost

Apr 04

Formal_SSA

Jan 17

UPF

Jan 08

2016

Card_Multisets

Dec 29

Bell_Numbers_Spivey

Dec 29

Ordinal

Nov 12

Iptables_Semantics

Oct 21

Subresultants

Oct 14

Efficient-Mergesort

Oct 14

Routing

Sep 09

Simple_Firewall

Aug 31

IP_Addresses

Aug 24

Separation_Logic_Imperative_HOL

Aug 08

Dijkstra_Shortest_Path

Aug 08

Dependent_SIFUM_Type_Systems

Jun 28

Noninterference_Sequential_Composition

Jun 13

Rank_Nullity_Theorem

May 20

EdmondsKarp_Maxflow

May 09

Noninterference_Ipurge_Unwinding

Apr 26

Boolean_Expression_Checkers

Mar 01

Slicing

Feb 05

Sqrt_Babylonian

Jan 29

Partial_Function_MR

Jan 29

2015

Marriage

Dec 02

Transitive-Closure

Nov 11

Simpl

Nov 11

Case_Labeling

Nov 11

KBPs

Sep 04

Echelon_Form

Jul 07

Noninterference_CSP

Jun 11

List_Interleaving

Jun 11

Coinductive_Languages

May 28

ConcurrentIMP

Apr 13

Heard_Of

Mar 18

Launchbury

Feb 20

Cayley_Hamilton

Feb 12

2014

AWN

Oct 23

Secondary_Sylow

Sep 09

Splay_Tree

Jul 07

Skew_Heap

Jul 07

Promela

May 28

Partial_Order_Reduction

May 28

LTL_to_GBA

May 28

Strong_Security

Apr 23

2013

Lehmer

Jul 22

Trie

Apr 15

Finger-Trees

Apr 15

Cauchy

Jan 03

2012

Gauss-Jordan-Elim-Fun

Jan 03

2011

LatticeProperties

Sep 22

Nat-Interval-Logic

Feb 23

2010

DataRefinementIBP

May 28

HRB-Slicing

Mar 23

2009

Binomial-Heaps

Nov 25

2007

Group-Ring-Module

Aug 08

2004

Lazy-Lists-II

Apr 26