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  
Approximation Approximation_Algorithms  
Concurrent ConcurrentGC  
Distributed DiskPaxos   GenClock   ClockSynchInst   Abortable_Linearizable_Modules   Heard_Of   Consensus_Refined   CRDT   IMAP-CRDT   OpSets   Stellar_Quorums   WOOT_Strong_Eventual_Consistency   Chandy_Lamport   Progress_Tracking  
Geometry Closest_Pair_Points  
Graph Depth-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  
Mathematical FFT   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  
Online List_Update  
Optimization Simplex  
Quantum computing Isabelle_Marries_Dirac   Projective_Measurements  

Artificial intelligence

Automata and formal languages

Concurrency

Data structures

Functional programming

Hardware

SPARCv8  

Machine learning

Networks

Programming languages

Decl_Sem_Fun_PL   Clean  
Compiling Compiling-Exceptions-Correctly   NormByEval   Density_Compiler   CakeML_Codegen   VeriComp   IMP_Compiler  
Lambda calculi POPLmark-deBruijn   Lam-ml-Normalization   PCF   Launchbury   LambdaMu   Higher_Order_Terms   Binding_Syntax_Theory   LambdaAuth  
Language definitions Jinja   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  
Logics Abstract-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  
Misc JiveDataStoreModel   Pop_Refinement   Case_Labeling   Interpreter_Optimizations  
Static analysis Program-Conflict-Analysis   Slicing   HRB-Slicing   Shivers-CFA   RIPEMD-160-SPARK   InfPathElimination   Abs_Int_ITP2012   Dominance_CHK  
Transformations WorkerWrapper   Call_Arity   Formal_SSA   Refine_Imperative_HOL   Minimal_SSA   Monad_Memo_DP  
Type systems MiniML   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

Analysis

Category theory

Combinatorics

Games and economics

Geometry

Graph theory

Misc

Number theory

Order

Physics

Probability theory

Topology

Tools