## 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