Index by Topic

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  

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

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  

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  

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

SPARCv8  

Deep_Learning  

UPF_Firewall   IP_Addresses   Simple_Firewall   Iptables_Semantics   Routing   LOFT  

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

Multi_Party_Computation   Noninterference_Generic_Unwinding   Noninterference_Ipurge_Unwinding   UPF   UPF_Firewall   CISC-Kernel   Noninterference_CSP   Key_Agreement_Strong_Adversaries   Security_Protocol_Refinement   Inductive_Confidentiality   Possibilistic_Noninterference   SIFUM_Type_Systems   Dependent_SIFUM_Type_Systems   Dependent_SIFUM_Refinement   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  

Launchbury   Clean   Transformer_Semantics   HOL-CSP   QHLProver   TESL_Language   Isabelle_C  

Circus   ComponentDependencies   Promela   Featherweight_OCL   DynamicArchitectures   Architectural_Design_Patterns   TESL_Language  

Propositional_Proof_Systems   MSO_Regex_Equivalence   Formula_Derivatives   Universal_Turing_Machine   Boolean_Expression_Checkers   Presburger-Automata   Verified-Prover   Completeness   Ordinal   Ordinals_and_Cardinals   FOL-Fitting   Epistemic_Logic   SequentInvertibility   LinearQuantifierElim   Nat-Interval-Logic   Recursion-Theory-I   Free-Boolean-Algebra   Sort_Encodings   LTL   HereditarilyFinite   Incompleteness   HyperCTL   Abstract_Completeness   PropResPI   SuperCalc   Incredible_Proof_Machine   Resolution_FOL   Surprise_Paradox   Allen_Calculus   Modal_Logics_for_NTS   Paraconsistency   FOL_Harrison   Abstract_Soundness   Differential_Dynamic_Logic   LambdaMu   Hybrid_Multi_Lane_Spatial_Logic   Ordered_Resolution_Prover   Minsky_Machines   Functional_Ordered_Resolution_Prover   Binding_Syntax_Theory   MFOTL_Monitor   FOL_Seq_Calc1   Hybrid_Logic  

GoedelGod   Types_Tableaus_and_Goedels_God   GewirthPGCProof   Lowe_Ontological_Argument   AnselmGod   PLM   Aristotles_Assertoric_Syllogistic  

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  

LatticeProperties   Stone_Algebras   Allen_Calculus   Order_Lattice_Props   Complete_Non_Orders   Szpilrajn  

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  

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

DiscretePricing   CryptHOL   Constructive_Cryptography   Probabilistic_While   Markov_Models   Density_Compiler   Probabilistic_Timed_Automata   Hidden_Markov_Models   Random_Graph_Subgraph_Threshold   Ergodic_Theory   Source_Coding_Theorem   Buffons_Needle  

Arith_Prog_Rel_Primes   Pell   Minkowskis_Theorem   E_Transcendental   Pi_Transcendental   Liouville_Numbers   Prime_Harmonic_Series   Fermat3_4   Perfect-Number-Thm   SumSquares   Lehmer   Pratt_Certificate   Dirichlet_Series   Gauss_Sums   Zeta_Function   Stern_Brocot   Bertrands_Postulate   Bernoulli   Diophantine_Eqns_Lin_Hom   Dirichlet_L   Mersenne_Primes   Irrationality_J_Hancl   Prime_Number_Theorem   Probabilistic_Prime_Tests   Prime_Distribution_Elementary   Transcendence_Series_Hancl_Rucki   Zeta_3_Irrational  

DiscretePricing   ArrowImpossibilityGS   SenSocialChoice   Vickrey_Clarke_Groves   Parity_Game   First_Welfare_Theorem   Randomised_Social_Choice   SDS_Impossibility   Stable_Matching   Fishburn_Impossibility   Neumann_Morgenstern_Utility  

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   Knot_Theory   Kuratowski_Closure_Complement   Smooth_Manifolds  

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  

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  

Category3   MonoidalCategory   Category   Category2   AxiomaticCategoryTheory   Bicategory  

No_FTL_observers  

ZFC_in_HOL  

FunWithFunctions   FunWithTilings   IMO2019  

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