Topics

Computer science

Algorithms

MuchAdoAboutTwo   SATSolverVerification   Efficient-Mergesort   Selection_Heap_Sort   Boolean_Expression_Checkers   Imperative_Insertion_Sort   TortoiseHare   Formal_SSA   CYK   ROBDD   Fisher_Yates   Comparison_Sort_Lower_Bound   Quick_Sort_Cost   Probabilistic_While   Knuth_Morris_Pratt   Median_Of_Medians_Selection   First_Order_Terms   VerifyThis2018   Monad_Memo_DP   Hidden_Markov_Models   Optimal_BST   Auto2_Imperative_HOL   IMP2   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   MDP-Algorithms   Gale_Shapley   VYDRA_MDL   Universal_Hash_Families   Prefix_Free_Code_Combinators  
ApproximationApproximation_Algorithms   Frequency_Moments  
ConcurrentConcurrentGC  
DistributedDiskPaxos   GenClock   ClockSynchInst   Abortable_Linearizable_Modules   Heard_Of   Consensus_Refined   CRDT   IMAP-CRDT   OpSets   Stellar_Quorums   WOOT_Strong_Eventual_Consistency   Chandy_Lamport   Progress_Tracking  
GeometryClosest_Pair_Points  
GraphDepth-First-Search   GraphMarkingIBP   Transitive-Closure   Dijkstra_Shortest_Path   Transitive-Closure-II   Roy_Floyd_Warshall   Gabow_SCC   DFS_Framework   EdmondsKarp_Maxflow   Floyd_Warshall   Prpu_Maxflow   Kruskal   Prim_Dijkstra_Simple   Relational_Minimum_Spanning_Trees  
MathematicalFFT   Polynomials   Gauss-Jordan-Elim-Fun   Gauss_Jordan   UpDown_Scheme   Echelon_Form   QR_Decomposition   Hermite   Groebner_Bases   Diophantine_Eqns_Lin_Hom   Taylor_Models   LLL_Basis_Reduction   Signature_Groebner   Smith_Normal_Form   Safe_Distance   Modular_arithmetic_LLL_and_HNF_algorithms   BenOr_Kozen_Reif   Virtual_Substitution   Equivalence_Relation_Enumeration  
OnlineList_Update  
OptimizationSimplex  
Quantum computingIsabelle_Marries_Dirac   Projective_Measurements   Registers  

Artificial intelligence

Automata and formal languages

Concurrency

Data structures

Functional programming

Hardware

Machine learning

Networks

Programming languages

Decl_Sem_Fun_PL   Clean  
CompilingCompiling-Exceptions-Correctly   NormByEval   Density_Compiler   CakeML_Codegen   VeriComp   IMP_Compiler  
Lambda calculiPOPLmark-deBruijn   Lam-ml-Normalization   PCF   Launchbury   LambdaMu   Higher_Order_Terms   Binding_Syntax_Theory   LambdaAuth   ResiduatedTransitionSystem  
Language definitionsJinja   FeatherweightJava   CoreC++   JinjaThreads   Simpl   Locally-Nameless-Sigma   LightweightJava   AutoFocus-Stream   FocusStreamsCaseStudies   GPU_Kernel_PL   pGCL   Isabelle_Meta_Model   Complx   CakeML   WebAssembly   Safe_OCL   Isabelle_C   JinjaDCI  
LogicsAbstract-Hoare-Logics   Simpl   SIFPL   BytecodeLogicJmlTypes   DataRefinementIBP   MonoBoolTranAlgebra   TLA   Refine_Monadic   Separation_Algebra   Separation_Logic_Imperative_HOL   Kleene_Algebra   Ribbon_Proofs   Automatic_Refinement   KAT_and_DRA   RefinementReactive   ConcurrentIMP   KAD   Separata   Complx   Differential_Dynamic_Logic   Hoare_Time   IMP2   UTP   QHLProver   Differential_Game_Logic   Relational-Incorrectness-Logic   Correctness_Algebras   Registers  
MiscJiveDataStoreModel   Pop_Refinement   Case_Labeling   Interpreter_Optimizations  
Static analysisProgram-Conflict-Analysis   Slicing   HRB-Slicing   Shivers-CFA   RIPEMD-160-SPARK   InfPathElimination   Abs_Int_ITP2012   Dominance_CHK  
TransformationsWorkerWrapper   Call_Arity   Formal_SSA   Refine_Imperative_HOL   Minimal_SSA   Monad_Memo_DP  
Type systemsMiniML   VolpanoSmith   Possibilistic_Noninterference   SIFUM_Type_Systems   WHATandWHERE_Security   Strong_Security   Dependent_SIFUM_Type_Systems   Name_Carrying_Type_Inference   Physical_Quantities   MiniSail  

Security

Semantics

System description languages

Logic

Computability

General logic

Philosophical aspects

Proof theory

Rewriting

Set theory

Mathematics

Algebra

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

Analysis

Category theory

Combinatorics

Games and economics

Geometry

Graph theory

Misc

Number theory

Order

Physics

Probability theory

Topology

Tools