diff --git a/web/statistics.html b/web/statistics.html --- a/web/statistics.html +++ b/web/statistics.html @@ -1,302 +1,307 @@ Archive of Formal Proofs

 

 

 

Home
About
Submission
Updating Entries
Using Entries
Search
Statistics
Index
Download

 

 

 

Statistics

 

Statistics

- - - - + + + +
Number of Articles:602
Number of Authors:386
Number of lemmas:~171,100
Lines of Code:~2,999,000
Number of Articles:607
Number of Authors:390
Number of lemmas:~171,200
Lines of Code:~2,993,400

Most used AFP articles:

+ + + + + - - - - - + - + - + + + + +
NameUsed by ? articles
1. List-Index 18
2.Show13
3.Coinductive 12
Collections 12
Regular-Sets 12
Show12
3.
4. Landau_Symbols 11
4.
5. Jordan_Normal_Form 10
Polynomial_Factorization 10
5.
6. Abstract-Rewriting 9
Automatic_Refinement 9
Deriving 9
Native_Word9

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,968 +1,968 @@ 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  

Algorithms

Knuth_Morris_Pratt   Probabilistic_While   Comparison_Sort_Lower_Bound   Quick_Sort_Cost   TortoiseHare   Selection_Heap_Sort   VerifyThis2018   CYK   Boolean_Expression_Checkers   Efficient-Mergesort   SATSolverVerification   MuchAdoAboutTwo   First_Order_Terms   Monad_Memo_DP   Hidden_Markov_Models   Imperative_Insertion_Sort   Formal_SSA   ROBDD   Median_Of_Medians_Selection   Fisher_Yates   Optimal_BST   IMP2   Auto2_Imperative_HOL   List_Inversions   IMP2_Binary_Heap   MFOTL_Monitor   Adaptive_State_Counting   Generic_Join   VerifyThis2019   Generalized_Counting_Sort   MFODL_Monitor_Optimized   Sliding_Window_Algorithm   PAC_Checker   Regression_Test_Selection   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   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   Optimization: Simplex   Quantum computing: Isabelle_Marries_Dirac   Projective_Measurements  

Concurrency

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

Data structures

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

Functional programming

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

Hardware

SPARCv8  

Machine learning

Deep_Learning   Inductive_Inference  

Networks

UPF_Firewall   IP_Addresses   Simple_Firewall   Iptables_Semantics   Routing   LOFT  

Programming languages

Clean   Decl_Sem_Fun_PL   Language definitions: CakeML   WebAssembly   pGCL   GPU_Kernel_PL   LightweightJava   CoreC++   FeatherweightJava   Jinja   JinjaThreads   Locally-Nameless-Sigma   AutoFocus-Stream   FocusStreamsCaseStudies   Isabelle_Meta_Model   Simpl   Complx   Safe_OCL   Isabelle_C   JinjaDCI   Lambda calculi: Higher_Order_Terms   Launchbury   PCF   POPLmark-deBruijn   Lam-ml-Normalization   LambdaMu   Binding_Syntax_Theory   LambdaAuth   Type systems: Name_Carrying_Type_Inference   MiniML   Possibilistic_Noninterference   SIFUM_Type_Systems   Dependent_SIFUM_Type_Systems   Strong_Security   WHATandWHERE_Security   VolpanoSmith   Physical_Quantities   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   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   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   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  

System description languages

Circus   ComponentDependencies   Promela   Featherweight_OCL   DynamicArchitectures   Architectural_Design_Patterns   TESL_Language  

Logic

Philosophical aspects

GoedelGod   Types_Tableaus_and_Goedels_God   GewirthPGCProof   Lowe_Ontological_Argument   AnselmGod   PLM   Aristotles_Assertoric_Syllogistic   Mereology  

General logic

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

Computability

Universal_Turing_Machine   Recursion-Theory-I   Inductive_Inference   Minsky_Machines  

Set theory

Ordinal   Ordinals_and_Cardinals   HereditarilyFinite   ZFC_in_HOL   Forcing   Delta_System_Lemma   Recursion-Addition   Ordinal_Partitions  

Proof theory

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

Rewriting

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

Mathematics

Order

LatticeProperties   Stone_Algebras   Allen_Calculus   Order_Lattice_Props   Complete_Non_Orders   Szpilrajn  

Algebra

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

Analysis

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

Probability theory

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

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  

Games and economics

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

Geometry

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

Topology

Topology   Knot_Theory   Kuratowski_Closure_Complement   Smooth_Manifolds  

Graph theory

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

Combinatorics

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

Category theory

Category3   MonoidalCategory   Category   Category2   AxiomaticCategoryTheory   Bicategory  

Physics

No_FTL_observers   Safe_Distance   Physical_Quantities   Quantum information: Isabelle_Marries_Dirac   Projective_Measurements  

Misc

FunWithFunctions   FunWithTilings   IMO2019  

Tools

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