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

 

 

 

Home
About
Submission
Updating Entries
Using Entries
Search
Statistics
Index
Download

 

 

 

Statistics

 

Statistics

- - + +
Number of Articles:478
Number of Authors:323
Number of lemmas:~133,900
Lines of Code:~2,256,600
Number of lemmas:~134,000
Lines of Code:~2,257,800

Most used AFP articles:

NameUsed by ? articles
1. Collections 15
2. List-Index 14
3. Coinductive 12
Regular-Sets 12
Show 12
4. Landau_Symbols 11
5. Abstract-Rewriting 10
Deriving 10
6. Automatic_Refinement 9
7. CAVA_Automata 8
8. Jordan_Normal_Form 7
Native_Word 7
Polynomial_Factorization 7

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,773 +1,776 @@ Archive of Formal Proofs

 

 

 

Home
About
Submission
Updating Entries
Using Entries
Search
Statistics
Index
Download

 

 

 

Index by Topic

 

Computer Science

Automata and Formal Languages

Partial_Order_Reduction   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  

Algorithms

Knuth_Morris_Pratt   Probabilistic_While   Comparison_Sort_Lower_Bound   Quick_Sort_Cost   DFS_Framework   Prpu_Maxflow   TortoiseHare   Floyd_Warshall   Roy_Floyd_Warshall   Selection_Heap_Sort   Dijkstra_Shortest_Path   EdmondsKarp_Maxflow   VerifyThis2018   CYK   Boolean_Expression_Checkers   Depth-First-Search   FFT   Gauss-Jordan-Elim-Fun   UpDown_Scheme   GraphMarkingIBP   Efficient-Mergesort   SATSolverVerification   Transitive-Closure   Transitive-Closure-II   MuchAdoAboutTwo   First_Order_Terms   Polynomials   Gabow_SCC   Monad_Memo_DP   Hidden_Markov_Models   Gauss_Jordan   Echelon_Form   QR_Decomposition   Hermite   Imperative_Insertion_Sort   Deep_Learning   Formal_SSA   ROBDD   Groebner_Bases   Median_Of_Medians_Selection   IMAP-CRDT   Fisher_Yates   Diophantine_Eqns_Lin_Hom   Taylor_Models   LLL_Basis_Reduction   Optimal_BST   Simplex   Signature_Groebner   IMP2   Auto2_Imperative_HOL   Kruskal   List_Inversions   IMP2_Binary_Heap   Distributed: DiskPaxos   GenClock   ClockSynchInst   Heard_Of   Consensus_Refined   Abortable_Linearizable_Modules   CRDT   OpSets   Concurrent: ConcurrentGC   Online: List_Update  

Concurrency

FLP   Concurrent_Ref_Alg   Concurrent_Revisions   Store_Buffer_Reduction   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  

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   Weight_Balanced_Trees   OpSets   Optimal_BST   Core_DOM   Auto2_Imperative_HOL   IMP2_Binary_Heap  

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  

Games

Parity_Game  

Hardware

SPARCv8  

Networks

UPF_Firewall   IP_Addresses   Simple_Firewall   Iptables_Semantics   Routing   LOFT  

Programming Languages

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   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   Logics: ConcurrentIMP   Refine_Monadic   Automatic_Refinement   MonoBoolTranAlgebra   Simpl   Separation_Algebra   Separation_Logic_Imperative_HOL   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   Compiling: Compiling-Exceptions-Correctly   NormByEval   Density_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  

Security

Multi_Party_Computation   Noninterference_Generic_Unwinding   Noninterference_Ipurge_Unwinding   UPF   UPF_Firewall   CISC-Kernel   Noninterference_CSP   Key_Agreement_Strong_Adversaries   Security_Protocol_Refinement   Inductive_Confidentiality   Possibilistic_Noninterference   SIFUM_Type_Systems   Dependent_SIFUM_Type_Systems   Dependent_SIFUM_Refinement   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   Cryptography: Game_Based_Crypto   CryptHOL   Constructive_Cryptography   RSAPSS   Elliptic_Curves_Group_Law  

Semantics

Launchbury   Transformer_Semantics   HOL-CSP   QHLProver  

System Description Languages

Circus   ComponentDependencies   Promela   Featherweight_OCL   DynamicArchitectures   Architectural_Design_Patterns  

Logic

Propositional_Proof_Systems   MSO_Regex_Equivalence   Formula_Derivatives   Universal_Turing_Machine   Boolean_Expression_Checkers   Presburger-Automata   Verified-Prover   Completeness   Ordinal   Ordinals_and_Cardinals   FOL-Fitting   Epistemic_Logic   SequentInvertibility   LinearQuantifierElim   Nat-Interval-Logic   Recursion-Theory-I   Free-Boolean-Algebra   Sort_Encodings   LTL   HereditarilyFinite   Incompleteness   HyperCTL   Abstract_Completeness   PropResPI   SuperCalc   Incredible_Proof_Machine   Resolution_FOL   Surprise_Paradox   Allen_Calculus   Modal_Logics_for_NTS   Paraconsistency   FOL_Harrison   Abstract_Soundness   Differential_Dynamic_Logic   LambdaMu   Hybrid_Multi_Lane_Spatial_Logic   Ordered_Resolution_Prover   Minsky_Machines   Functional_Ordered_Resolution_Prover   Binding_Syntax_Theory  

Philosophy

GoedelGod   Types_Tableaus_and_Goedels_God   GewirthPGCProof   Lowe_Ontological_Argument   AnselmGod   PLM  

Rewriting

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  

Mathematics

-

Algebra

+

Order

+
+ LatticeProperties   +
+

Algebra

Optics   Subresultants   Buildings   Algebraic_VCs   Multirelations   Residuated_Lattices   PseudoHoops   - LatticeProperties   Impossible_Geometry   Gauss-Jordan-Elim-Fun   Matrix_Tensor   Stone_Algebras   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   Allen_Calculus   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   Order_Lattice_Props   Quantales   Transformer_Semantics   Farkas   Groebner_Macaulay   Linear_Inequalities  

Analysis

E_Transcendental   Liouville_Numbers   Descartes_Sign_Rule   Euler_MacLaurin   Real_Impl   Lower_Semicontinuous   Affine_Arithmetic   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   Cartan_FP   Stirling_Formula   Lp   Bernoulli   Winding_Number_Eval   Count_Complex_Roots   Taylor_Models   Green   Irrationality_J_Hancl   Budan_Fourier   Smooth_Manifolds   Transcendence_Series_Hancl_Rucki  

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  

Number Theory

Pell   Minkowskis_Theorem   E_Transcendental   Pi_Transcendental   Liouville_Numbers   Prime_Harmonic_Series   Fermat3_4   Perfect-Number-Thm   SumSquares   Lehmer   Pratt_Certificate   Dirichlet_Series   Zeta_Function   Stern_Brocot   Bertrands_Postulate   Bernoulli   Diophantine_Eqns_Lin_Hom   Dirichlet_L   Irrationality_J_Hancl   Prime_Number_Theorem   Probabilistic_Prime_Tests   Prime_Distribution_Elementary   Transcendence_Series_Hancl_Rucki  

Economics

DiscretePricing   ArrowImpossibilityGS   SenSocialChoice   Vickrey_Clarke_Groves   First_Welfare_Theorem   Randomised_Social_Choice   SDS_Impossibility   Stable_Matching   Fishburn_Impossibility   Neumann_Morgenstern_Utility  

Geometry

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

Topology

Topology   Knot_Theory   Kuratowski_Closure_Complement   Smooth_Manifolds  

Graph Theory

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

Combinatorics

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

Category Theory

Category3   MonoidalCategory   Category   Category2   AxiomaticCategoryTheory  

Physics

No_FTL_observers  

Misc

FunWithFunctions   FunWithTilings  

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  
\ No newline at end of file