Index by Topic

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   Approximation Approximation_Algorithms   Approximation_Algorithms   Concurrent ConcurrentGC   ConcurrentGC   Distributed DiskPaxos   DiskPaxos   GenClock   GenClock   ClockSynchInst   ClockSynchInst   Abortable_Linearizable_Modules   Abortable_Linearizable_Modules   Heard_Of   Heard_Of   Consensus_Refined   Consensus_Refined   CRDT   CRDT   IMAP-CRDT   IMAP-CRDT   OpSets   OpSets   Stellar_Quorums   Stellar_Quorums   WOOT_Strong_Eventual_Consistency   WOOT_Strong_Eventual_Consistency   Chandy_Lamport   Chandy_Lamport   Geometry Closest_Pair_Points   Closest_Pair_Points   Graph Depth-First-Search   Depth-First-Search   GraphMarkingIBP   GraphMarkingIBP   Transitive-Closure   Transitive-Closure   Dijkstra_Shortest_Path   Dijkstra_Shortest_Path   Transitive-Closure-II   Transitive-Closure-II   Roy_Floyd_Warshall   Roy_Floyd_Warshall   Gabow_SCC   Gabow_SCC   DFS_Framework   DFS_Framework   EdmondsKarp_Maxflow   EdmondsKarp_Maxflow   Floyd_Warshall   Floyd_Warshall   Prpu_Maxflow   Prpu_Maxflow   Kruskal   Kruskal   Prim_Dijkstra_Simple   Prim_Dijkstra_Simple   Mathematical FFT   FFT   Polynomials   Polynomials   Gauss-Jordan-Elim-Fun   Gauss-Jordan-Elim-Fun   Gauss_Jordan   Gauss_Jordan   UpDown_Scheme   UpDown_Scheme   Echelon_Form   Echelon_Form   QR_Decomposition   QR_Decomposition   Hermite   Hermite   Groebner_Bases   Groebner_Bases   Diophantine_Eqns_Lin_Hom   Diophantine_Eqns_Lin_Hom   Taylor_Models   Taylor_Models   LLL_Basis_Reduction   LLL_Basis_Reduction   Signature_Groebner   Signature_Groebner   Smith_Normal_Form   Smith_Normal_Form   Safe_Distance   Safe_Distance   Online List_Update   List_Update   Optimization Simplex   Simplex  

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  

FLP   Concurrent_Ref_Alg   Concurrent_Revisions   Store_Buffer_Reduction   TESL_Language   Process calculi Circus   Circus   CCS   CCS   Psi_Calculi   Psi_Calculi   Pi_Calculus   Pi_Calculus   AWN   AWN   AODV   AODV   Noninterference_Generic_Unwinding   Noninterference_Generic_Unwinding   Encodability_Process_Calculi   Encodability_Process_Calculi   Noninterference_Sequential_Composition   Noninterference_Sequential_Composition   Noninterference_Concurrent_Composition   Noninterference_Concurrent_Composition   Modal_Logics_for_NTS   Modal_Logics_for_NTS   HOL-CSP   HOL-CSP  

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  

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  

SPARCv8  

Deep_Learning   Inductive_Inference  

IP_Addresses   Simple_Firewall   Routing   Iptables_Semantics   LOFT   UPF_Firewall  

Decl_Sem_Fun_PL   Clean   Compiling Compiling-Exceptions-Correctly   Compiling-Exceptions-Correctly   NormByEval   NormByEval   Density_Compiler   Density_Compiler   CakeML_Codegen   CakeML_Codegen   VeriComp   VeriComp   Lambda calculi POPLmark-deBruijn   POPLmark-deBruijn   Lam-ml-Normalization   Lam-ml-Normalization   PCF   PCF   Launchbury   Launchbury   LambdaMu   LambdaMu   Higher_Order_Terms   Higher_Order_Terms   Binding_Syntax_Theory   Binding_Syntax_Theory   LambdaAuth   LambdaAuth   Language definitions Jinja   Jinja   FeatherweightJava   FeatherweightJava   CoreC++   CoreC++   JinjaThreads   JinjaThreads   Simpl   Simpl   Locally-Nameless-Sigma   Locally-Nameless-Sigma   LightweightJava   LightweightJava   AutoFocus-Stream   AutoFocus-Stream   FocusStreamsCaseStudies   FocusStreamsCaseStudies   GPU_Kernel_PL   GPU_Kernel_PL   pGCL   pGCL   Isabelle_Meta_Model   Isabelle_Meta_Model   Complx   Complx   CakeML   CakeML   WebAssembly   WebAssembly   Safe_OCL   Safe_OCL   Isabelle_C   Isabelle_C   Logics Abstract-Hoare-Logics   Abstract-Hoare-Logics   Simpl   Simpl   SIFPL   SIFPL   BytecodeLogicJmlTypes   BytecodeLogicJmlTypes   DataRefinementIBP   DataRefinementIBP   MonoBoolTranAlgebra   MonoBoolTranAlgebra   TLA   TLA   Refine_Monadic   Refine_Monadic   Separation_Algebra   Separation_Algebra   Separation_Logic_Imperative_HOL   Separation_Logic_Imperative_HOL   Kleene_Algebra   Kleene_Algebra   Ribbon_Proofs   Ribbon_Proofs   Automatic_Refinement   Automatic_Refinement   KAT_and_DRA   KAT_and_DRA   RefinementReactive   RefinementReactive   ConcurrentIMP   ConcurrentIMP   KAD   KAD   Separata   Separata   Complx   Complx   Differential_Dynamic_Logic   Differential_Dynamic_Logic   Hoare_Time   Hoare_Time   IMP2   IMP2   UTP   UTP   QHLProver   QHLProver   Differential_Game_Logic   Differential_Game_Logic   Relational-Incorrectness-Logic   Relational-Incorrectness-Logic   Misc JiveDataStoreModel   JiveDataStoreModel   Pop_Refinement   Pop_Refinement   Case_Labeling   Case_Labeling   Static analysis Program-Conflict-Analysis   Program-Conflict-Analysis   Slicing   Slicing   HRB-Slicing   HRB-Slicing   Shivers-CFA   Shivers-CFA   RIPEMD-160-SPARK   RIPEMD-160-SPARK   InfPathElimination   InfPathElimination   Abs_Int_ITP2012   Abs_Int_ITP2012   Transformations WorkerWrapper   WorkerWrapper   Call_Arity   Call_Arity   Formal_SSA   Formal_SSA   Refine_Imperative_HOL   Refine_Imperative_HOL   Minimal_SSA   Minimal_SSA   Monad_Memo_DP   Monad_Memo_DP   Type systems MiniML   MiniML   VolpanoSmith   VolpanoSmith   Possibilistic_Noninterference   Possibilistic_Noninterference   SIFUM_Type_Systems   SIFUM_Type_Systems   WHATandWHERE_Security   WHATandWHERE_Security   Strong_Security   Strong_Security   Dependent_SIFUM_Type_Systems   Dependent_SIFUM_Type_Systems   Name_Carrying_Type_Inference   Name_Carrying_Type_Inference  

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   Cryptography RSAPSS   RSAPSS   Elliptic_Curves_Group_Law   Elliptic_Curves_Group_Law   CryptHOL   CryptHOL   Game_Based_Crypto   Game_Based_Crypto   Constructive_Cryptography   Constructive_Cryptography   Sigma_Commit_Crypto   Sigma_Commit_Crypto  

Launchbury   Transformer_Semantics   QHLProver   HOL-CSP   TESL_Language   Clean   Isabelle_C  

Circus   Featherweight_OCL   ComponentDependencies   Promela   DynamicArchitectures   Architectural_Design_Patterns   TESL_Language  

Recursion-Theory-I   Minsky_Machines   Universal_Turing_Machine   Inductive_Inference  

Classical first-order logic FOL-Fitting   Classical propositional logic Free-Boolean-Algebra   Decidability of theories LinearQuantifierElim   Presburger-Automata   MSO_Regex_Equivalence   Formula_Derivatives   Lambda calculus LambdaMu   Logics of knowledge and belief Epistemic_Logic   Mechanization of proofs Verified-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   Modal logic Modal_Logics_for_NTS   Differential_Dynamic_Logic   Hybrid_Multi_Lane_Spatial_Logic   Hybrid_Logic   MFODL_Monitor_Optimized   Paraconsistent logics Paraconsistency   Temporal logic Nat-Interval-Logic   HyperCTL   LTL   Allen_Calculus   MFOTL_Monitor   LTL_Normal_Form  

GoedelGod   Types_Tableaus_and_Goedels_God   AnselmGod   PLM   Lowe_Ontological_Argument   GewirthPGCProof   Aristotles_Assertoric_Syllogistic  

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  

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  

Ordinal   Ordinals_and_Cardinals   HereditarilyFinite   ZFC_in_HOL   Forcing   Recursion-Addition   Ordinal_Partitions  

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  

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  

Category   Category2   Category3   MonoidalCategory   AxiomaticCategoryTheory   Bicategory  

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  

ArrowImpossibilityGS   SenSocialChoice   Vickrey_Clarke_Groves   Parity_Game   SDS_Impossibility   Randomised_Social_Choice   Stable_Matching   First_Welfare_Theorem   Fishburn_Impossibility   Neumann_Morgenstern_Utility   DiscretePricing  

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  

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  

FunWithFunctions   FunWithTilings   IMO2019  

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  

LatticeProperties   Stone_Algebras   Allen_Calculus   Order_Lattice_Props   Complete_Non_Orders   Szpilrajn  

No_FTL_observers   Safe_Distance  

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  

Topology   Knot_Theory   Kuratowski_Closure_Complement   Smooth_Manifolds  

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