Index by Topic

Computer Science

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

Algorithms

Knuth_Morris_Pratt Probabilistic_While Comparison_Sort_Lower_Bound Quick_Sort_Cost TortoiseHare Selection_Heap_Sort VerifyThis2018 CYK Boolean_Expression_Checkers FFT Gauss-Jordan-Elim-Fun UpDown_Scheme Efficient-Mergesort SATSolverVerification MuchAdoAboutTwo First_Order_Terms Polynomials 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 List_Inversions IMP2_Binary_Heap MFOTL_Monitor Adaptive_State_Counting Generic_Join VerifyThis2019 Generalized_Counting_Sort 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 Distributed: DiskPaxos GenClock ClockSynchInst Heard_Of Consensus_Refined Abortable_Linearizable_Modules CRDT OpSets Stellar_Quorums Concurrent: ConcurrentGC Online: List_Update + Optimization: + Simplex

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

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 Auto2_Imperative_HOL IMP2_Binary_Heap Priority_Search_Trees Interval_Arithmetic_Word32

Functional Programming

Games

Parity_Game

Hardware

SPARCv8

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 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 Differential_Game_Logic Compiling: CakeML_Codegen 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 Sigma_Commit_Crypto CryptHOL Constructive_Cryptography RSAPSS Elliptic_Curves_Group_Law

Semantics

Launchbury Clean Transformer_Semantics HOL-CSP QHLProver TESL_Language Isabelle_C

System Description Languages

Circus ComponentDependencies Promela Featherweight_OCL DynamicArchitectures Architectural_Design_Patterns TESL_Language

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 MFOTL_Monitor FOL_Seq_Calc1 Hybrid_Logic

Philosophy

GoedelGod Types_Tableaus_and_Goedels_God GewirthPGCProof Lowe_Ontological_Argument AnselmGod PLM Aristotles_Assertoric_Syllogistic

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

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

Analysis

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 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 Hybrid_Systems_VCs Poincare_Bendixson

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

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 Bicategory

Physics

No_FTL_observers

Set Theory

ZFC_in_HOL

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