Index by Topic

 

Computer science

Artificial intelligence

Automata and formal languages

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   MDP-Algorithms   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   Gale_Shapley   VYDRA_MDL   Universal_Hash_Families   Prefix_Free_Code_Combinators   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   Frequency_Moments   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   Virtual_Substitution   Equivalence_Relation_Enumeration   Optimization: Simplex   Quantum computing: Isabelle_Marries_Dirac   Projective_Measurements   Registers  

Concurrency

Data structures

Functional programming

Hardware

Machine learning

Networks

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   ResiduatedTransitionSystem   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   Package_logic   Combinable_Wands   Correctness_Algebras   Registers   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   Dominance_CHK   Transformations: Call_Arity   Refine_Imperative_HOL   WorkerWrapper   Monad_Memo_DP   Formal_SSA   Minimal_SSA   Misc: JiveDataStoreModel   Pop_Refinement   Case_Labeling   Interpreter_Optimizations  

Security

Semantics

System description languages

Logic

Philosophical aspects

General logic

Computability

Set theory

Proof theory

Rewriting

Mathematics

Order

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   Finitely_Generated_Abelian_Groups   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   Factor_Algebraic_Polynomial   Hyperdual   Interpolation_Polynomials_HOL_Algebra   LP_Duality   Fishers_Inequality   Finite_Fields  

Analysis

Measure theory

Probability theory

Number theory

Games and economics

Geometry

Topology

Graph theory

Combinatorics

Category theory

Physics

Misc

Tools