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 MFODL_Monitor_Optimized

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 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 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 IMAP-CRDT CRDT OpSets Stellar_Quorums WOOT_Strong_Eventual_Consistency Concurrent: ConcurrentGC Online: List_Update Geometry: Closest_Pair_Points Approximation: Approximation_Algorithms 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 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 ADS_Functor

Functional Programming

Hardware

SPARCv8

Machine Learning

Deep_Learning

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 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 Compiling: CakeML_Codegen Compiling-Exceptions-Correctly NormByEval Density_Compiler VeriComp 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 Attack_Trees Inductive_Confidentiality Possibilistic_Noninterference SIFUM_Type_Systems Dependent_SIFUM_Type_Systems Dependent_SIFUM_Refinement Relational-Incorrectness-Logic 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

Philosophical aspects

GoedelGod Types_Tableaus_and_Goedels_God GewirthPGCProof Lowe_Ontological_Argument AnselmGod PLM Aristotles_Assertoric_Syllogistic

General logic

Classical propositional logic: Free-Boolean-Algebra Classical first-order logic: FOL-Fitting Decidability of theories: MSO_Regex_Equivalence Formula_Derivatives Presburger-Automata LinearQuantifierElim Mechanization of proofs: Boolean_Expression_Checkers Verified-Prover Sort_Encodings PropResPI Resolution_FOL FOL_Harrison Ordered_Resolution_Prover Functional_Ordered_Resolution_Prover Binding_Syntax_Theory Saturation_Framework Lambda calculus: LambdaMu Logics of knowledge and belief: Epistemic_Logic Temporal logic: Nat-Interval-Logic LTL HyperCTL Allen_Calculus MFOTL_Monitor Modal logic: Modal_Logics_for_NTS Differential_Dynamic_Logic Hybrid_Multi_Lane_Spatial_Logic Hybrid_Logic MFODL_Monitor_Optimized Paraconsistent logics: Paraconsistency

Computability

Universal_Turing_Machine Recursion-Theory-I Minsky_Machines

Set theory

Ordinal Ordinals_and_Cardinals HereditarilyFinite + ZFC_in_HOL Forcing

Proof theory

Propositional_Proof_Systems Completeness SequentInvertibility Incompleteness Abstract_Completeness SuperCalc Incredible_Proof_Machine Surprise_Paradox Abstract_Soundness FOL_Seq_Calc1

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 Goodstein_Lambda

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 Subset_Boolean_Algebras Power_Sum_Polynomials

Analysis

Banach_Steinhaus 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 Lambert_W Cartan_FP Deep_Learning 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

Geometry

Complex_Geometry Poincare_Disc 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 Parity_Game 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