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

AI_Planning_Languages_Semantics   Verified_SAT_Based_AI_Planning  

Automata and formal languages

Functional-Automata   Tree-Automata   Presburger-Automata   Regular-Sets   Statecharts   KBPs   Myhill-Nerode   Markov_Models   Stuttering_Equivalence   Kleene_Algebra   Coinductive_Languages   KAT_and_DRA   Regex_Equivalence   Regular_Algebras   CAVA_LTL_Modelchecker   LTL_to_GBA   CAVA_Automata   MSO_Regex_Equivalence   Finite_Automata_HF   Probabilistic_System_Zoo   Formula_Derivatives   LTL_to_DRA   LTL   Timed_Automata   KAD   CYK   Posix-Lexing   LocalLexing   Buchi_Complementation   Transition_Systems_and_Automata   Stochastic_Matrices   Probabilistic_Timed_Automata   Partial_Order_Reduction   Factored_Transition_System_Bounding   Universal_Turing_Machine   LTL_Master_Theorem   MFOTL_Monitor   C2KA_DistributedSystems   Adaptive_State_Counting   MFODL_Monitor_Optimized   LTL_Normal_Form   Extended_Finite_State_Machines   Extended_Finite_State_Machine_Inference   Combinatorics_Words   Combinatorics_Words_Graph_Lemma   Combinatorics_Words_Lyndon   Regular_Tree_Relations   FO_Theory_Rewriting   ResiduatedTransitionSystem  

Concurrency

FLP   Concurrent_Ref_Alg   Concurrent_Revisions   Store_Buffer_Reduction   TESL_Language   ResiduatedTransitionSystem  
Process calculiCircus   CCS   Psi_Calculi   Pi_Calculus   AWN   AODV   Noninterference_Generic_Unwinding   Encodability_Process_Calculi   Noninterference_Sequential_Composition   Noninterference_Concurrent_Composition   Modal_Logics_for_NTS   HOL-CSP   CSP_RefTK  

Data structures

AVL-Trees   BinarySearchTree   Lazy-Lists-II   FileRefinement   BDD   Huffman   FinFun   Collections   List-Index   Matrix   Binomial-Heaps   Finger-Trees   Binomial-Queues   List-Infinite   Datatype_Order_Generator   Containers   IEEE_Floating_Point   Native_Word   Amortized_Complexity   Splay_Tree   Skew_Heap   Priority_Queue_Braun   XML   Deriving   Trie   Dynamic_Tables   List_Interleaving   Matrix_Tensor   ROBDD   Word_Lib   Pairing_Heap   Refine_Imperative_HOL   Random_BSTs   CRDT   Root_Balanced_Tree   IMAP-CRDT   Taylor_Models   Treaps   Weight_Balanced_Trees   OpSets   Optimal_BST   Randomised_BSTs   Generic_Deriving   Auto2_Imperative_HOL   Core_DOM   KD_Tree   IMP2_Binary_Heap   Priority_Search_Trees   Interval_Arithmetic_Word32   Skip_Lists   ADS_Functor   Relational_Disjoint_Set_Forests   Shadow_DOM   Shadow_SC_DOM   SC_DOM_Components   DOM_Components   Core_SC_DOM   Finite-Map-Extras   Hood_Melville_Queue   BTree   Fresh_Identifiers   Van_Emde_Boas_Trees   Prefix_Free_Code_Combinators  

Functional programming

Stream-Fusion   Coinductive   Tycon   Tail_Recursive_Functions   Partial_Function_MR   Show   Certification_Monads   XML   Stream_Fusion_Code   Lifting_Definition_Option   Applicative_Lifting   CryptHOL   Monomorphic_Monad   Monad_Normalisation   Probabilistic_While   Optics   HOLCF-Prelude   BNF_CC   Monad_Memo_DP   Binding_Syntax_Theory   Generalized_Counting_Sort   Hello_World   BirdKMP  

Hardware

SPARCv8   X86_Semantics  

Machine learning

Deep_Learning   Inductive_Inference  

Networks

IP_Addresses   Simple_Firewall   Routing   Iptables_Semantics   LOFT   UPF_Firewall  

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

HotelKeyCards   VolpanoSmith   SIFPL   InformationFlowSlicing   InformationFlowSlicing_Inter   Inductive_Confidentiality   Possibilistic_Noninterference   CryptoBasedCompositionalProperties   Probabilistic_Noninterference   HyperCTL   Bounded_Deducibility_Security   SIFUM_Type_Systems   WHATandWHERE_Security   Strong_Security   Noninterference_CSP   Network_Security_Policy_Verification   CISC-Kernel   UPF   Noninterference_Generic_Unwinding   Noninterference_Ipurge_Unwinding   Noninterference_Inductive_Unwinding   Noninterference_Sequential_Composition   Noninterference_Concurrent_Composition   Dependent_SIFUM_Type_Systems   Dependent_SIFUM_Refinement   SPARCv8   Password_Authentication_Protocol   UPF_Firewall   Key_Agreement_Strong_Adversaries   Security_Protocol_Refinement   Modular_Assembly_Kit_Security   Multi_Party_Computation   LambdaAuth   Relational-Incorrectness-Logic   Automated_Stateful_Protocol_Verification   Stateful_Protocol_Composition_and_Typing   Attack_Trees   Relational_Method   IFC_Tracking   CoCon   BD_Security_Compositional   CoSMed   CoSMeDis   Logging_Independent_Anonymity  
CryptographyRSAPSS   Elliptic_Curves_Group_Law   CryptHOL   Game_Based_Crypto   Constructive_Cryptography   Sigma_Commit_Crypto   Constructive_Cryptography_CM  

Semantics

Launchbury   Transformer_Semantics   QHLProver   HOL-CSP   TESL_Language   Clean   Isabelle_C   CSP_RefTK   X86_Semantics   Registers   Quasi_Borel_Spaces  

System description languages

Circus   Featherweight_OCL   ComponentDependencies   Promela   DynamicArchitectures   Architectural_Design_Patterns   TESL_Language  

Logic

Computability

Recursion-Theory-I   Minsky_Machines   Universal_Turing_Machine   Inductive_Inference   Ackermanns_not_PR  

General logic

Topological_Semantics   Metalogic_ProofChecker  
Classical first-order logicFOL-Fitting   FOL_Axiomatic   FOL_Seq_Calc2   Eval_FO   FOL_Seq_Calc3  
Classical propositional logicFree-Boolean-Algebra  
Decidability of theoriesLinearQuantifierElim   Presburger-Automata   MSO_Regex_Equivalence   Formula_Derivatives  
Lambda calculusLambdaMu  
Logics of knowledge and beliefEpistemic_Logic   Blue_Eyes   Public_Announcement_Logic   Belief_Revision   PAL  
Mechanization of proofsVerified-Prover   Sort_Encodings   Boolean_Expression_Checkers   PropResPI   Resolution_FOL   FOL_Harrison   Ordered_Resolution_Prover   Functional_Ordered_Resolution_Prover   Binding_Syntax_Theory   Saturation_Framework   Saturation_Framework_Extensions   FOL_Seq_Calc2   FOL_Seq_Calc3  
Modal logicModal_Logics_for_NTS   Differential_Dynamic_Logic   Hybrid_Multi_Lane_Spatial_Logic   Hybrid_Logic   MFODL_Monitor_Optimized   SimplifiedOntologicalArgument  
Paraconsistent logicsParaconsistency  
Temporal logicNat-Interval-Logic   HyperCTL   LTL   Allen_Calculus   MFOTL_Monitor   LTL_Normal_Form  

Philosophical aspects

GoedelGod   Types_Tableaus_and_Goedels_God   AnselmGod   PLM   Lowe_Ontological_Argument   GewirthPGCProof   Aristotles_Assertoric_Syllogistic   Mereology   SimplifiedOntologicalArgument  

Proof theory

Completeness   SequentInvertibility   Incompleteness   Abstract_Completeness   Incredible_Proof_Machine   Surprise_Paradox   SuperCalc   Abstract_Soundness   Propositional_Proof_Systems   FOL_Seq_Calc1   Goedel_Incompleteness   Goedel_HFSet_Semantic   Goedel_HFSet_Semanticless   Robinson_Arithmetic   Syntax_Independent_Logic   FOL_Axiomatic   FOL_Seq_Calc2   FO_Theory_Rewriting   FOL_Seq_Calc3  

Rewriting

Abstract-Rewriting   Decreasing-Diagrams   Decreasing-Diagrams-II   Rewriting_Z   Lambda_Free_RPOs   Lambda_Free_KBOs   Nested_Multisets_Ordinals   Monad_Normalisation   First_Order_Terms   Lambda_Free_EPO   Graph_Saturation   CakeML_Codegen   Goodstein_Lambda   Knuth_Bendix_Order   Weighted_Path_Order   FO_Theory_Rewriting   Multiset_Ordering_NPC  

Set theory

Ordinal   Ordinals_and_Cardinals   HereditarilyFinite   ZFC_in_HOL   Forcing   Recursion-Addition   Ordinal_Partitions   Delta_System_Lemma   CZH_Foundations   Wetzels_Problem   Transitive_Models   Independence_CH  

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

Integration   Cauchy   Polynomials   Lower_Semicontinuous   Ordinary_Differential_Equations   Sqrt_Babylonian   Sturm_Sequences   Real_Impl   Affine_Arithmetic   Special_Function_Bounds   Sturm_Tarski   Landau_Symbols   Akra_Bazzi   Descartes_Sign_Rule   Liouville_Numbers   Cartan_FP   Stirling_Formula   Lp   Deep_Learning   E_Transcendental   Bernoulli   Euler_MacLaurin   Linear_Recurrences   Zeta_Function   Count_Complex_Roots   Winding_Number_Eval   Taylor_Models   Green   Error_Function   Irrationality_J_Hancl   Budan_Fourier   Smooth_Manifolds   Transcendence_Series_Hancl_Rucki   Laplace_Transform   Fourier   Hybrid_Systems_VCs   Poincare_Bendixson   Matrices_for_ODEs   Lambert_W   Banach_Steinhaus   Irrational_Series_Erdos_Straus   Three_Circles   Cubic_Quartic_Equations   Complex_Bounded_Operators   Real_Power   Hyperdual   Youngs_Inequality   Wetzels_Problem   Cotangent_PFD_Formula   Dedekind_Real   Sophomores_Dream  

Category theory

Category   Category2   Category3   MonoidalCategory   AxiomaticCategoryTheory   Bicategory   CZH_Foundations   CZH_Elementary_Categories   CZH_Universal_Constructions  

Combinatorics

Ramsey-Infinite   Marriage   Well_Quasi_Orders   Bondy   Open_Induction   Discrete_Summation   Derangements   Euler_Partition   Latin_Square   Card_Partitions   Card_Number_Partitions   Bell_Numbers_Spivey   Card_Equiv_Relations   Catalan_Numbers   Card_Multisets   Twelvefold_Way   Falling_Factorial_Sum   Matroids   Nash_Williams   Ordinal_Partitions   Delta_System_Lemma   Sunflowers   Van_der_Waerden   Design_Theory   Szemeredi_Regularity   Roth_Arithmetic_Progressions   Equivalence_Relation_Enumeration   Fishers_Inequality   Clique_and_Monotone_Circuits  

Games and economics

ArrowImpossibilityGS   SenSocialChoice   Vickrey_Clarke_Groves   Parity_Game   SDS_Impossibility   Randomised_Social_Choice   Stable_Matching   First_Welfare_Theorem   Fishburn_Impossibility   Neumann_Morgenstern_Utility   DiscretePricing   GaleStewart_Games   Gale_Shapley   Actuarial_Mathematics  

Geometry

General-Triangle   Impossible_Geometry   Tarskis_Geometry   Triangle   Buildings   Ptolemys_Theorem   Chord_Segments   Buffons_Needle   Minkowskis_Theorem   Stewart_Apollonius   Gromov_Hyperbolicity   Projective_Geometry   Quaternions   Octonions   Nullstellensatz   Complex_Geometry   Poincare_Disc   IsaGeoCoq   Grothendieck_Schemes   Schutz_Spacetime   Foundation_of_geometry  

Graph theory

Flyspeck-Tame   Max-Card-Matching   Girth_Chromatic   Graph_Theory   ShortestPath   Koenigsberg_Friendship   Random_Graph_Subgraph_Threshold   Gabow_SCC   Parity_Game   Planarity_Certificates   MFMC_Countable   Tree_Decomposition   Menger   Flow_Networks   Prpu_Maxflow   Factored_Transition_System_Bounding   Graph_Saturation   Relational_Paths   Relational_Forests   Szemeredi_Regularity   Roth_Arithmetic_Progressions   Knights_Tour  

Misc

FunWithFunctions   FunWithTilings   IMO2019  

Number theory

Fermat3_4   SumSquares   Perfect-Number-Thm   Lehmer   Pratt_Certificate   Stern_Brocot   Liouville_Numbers   Prime_Harmonic_Series   E_Transcendental   Bertrands_Postulate   Bernoulli   Minkowskis_Theorem   Dirichlet_Series   Zeta_Function   Diophantine_Eqns_Lin_Hom   Dirichlet_L   Irrationality_J_Hancl   Pell   Prime_Number_Theorem   Pi_Transcendental   Probabilistic_Prime_Tests   Prime_Distribution_Elementary   Transcendence_Series_Hancl_Rucki   Gauss_Sums   Zeta_3_Irrational   Mersenne_Primes   Arith_Prog_Rel_Primes   Furstenberg_Topology   Lucas_Theorem   Gaussian_Integers   Irrational_Series_Erdos_Straus   Amicable_Numbers   Hermite_Lindemann   Padic_Ints   Lifting_the_Exponent   Irrationals_From_THEBOOK   Digit_Expansions  

Order

LatticeProperties   Stone_Algebras   Allen_Calculus   Order_Lattice_Props   Complete_Non_Orders   Szpilrajn  

Physics

No_FTL_observers   Safe_Distance   Physical_Quantities   Schutz_Spacetime  
Quantum informationIsabelle_Marries_Dirac   Projective_Measurements  

Probability theory

Markov_Models   Random_Graph_Subgraph_Threshold   Density_Compiler   Ergodic_Theory   Source_Coding_Theorem   CryptHOL   Probabilistic_While   Buffons_Needle   Probabilistic_Timed_Automata   Hidden_Markov_Models   DiscretePricing   Constructive_Cryptography   Laws_of_Large_Numbers   Constructive_Cryptography_CM   MDP-Rewards   MDP-Algorithms   Median_Method   Universal_Hash_Families   Frequency_Moments  

Topology

Topology   Knot_Theory   Kuratowski_Closure_Complement   Smooth_Manifolds   Simplicial_complexes_and_boolean_functions  

Tools

DPT-SAT-Solver   Nominal2   Case_Labeling   Separata   Proof_Strategy_Language   Lazy_Case   Constructor_Funs   Monad_Normalisation   Dict_Construction   Diophantine_Eqns_Lin_Hom   BNF_Operations   BNF_CC   Auto2_HOL   Isabelle_C   Automated_Stateful_Protocol_Verification   SpecCheck   Conditional_Simplification   Conditional_Transfer_Rule   Types_To_Sets_Extension   Intro_Dest_Elim