Index by Topic

 

Computer Science

Automata and Formal Languages

Posix-Lexing   KBPs   Regular-Sets   Regex_Equivalence   MSO_Regex_Equivalence   Formula_Derivatives   Myhill-Nerode   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   Finite_Automata_HF   LTL_to_DRA   Timed_Automata  

Algorithms

DFS_Framework   TortoiseHare   Roy_Floyd_Warshall   Selection_Heap_Sort   Dijkstra_Shortest_Path   EdmondsKarp_Maxflow   CYK   Boolean_Expression_Checkers   Depth-First-Search   FFT   Gauss-Jordan-Elim-Fun   UpDown_Scheme   GraphMarkingIBP   Efficient-Mergesort   SATSolverVerification   Transitive-Closure   Transitive-Closure-II   MuchAdoAboutTwo   Gabow_SCC   Gauss_Jordan   Echelon_Form   QR_Decomposition   Hermite   Imperative_Insertion_Sort   Formal_SSA   ROBDD   Groebner_Bases   Multivariate_Polynomials   Distributed: DiskPaxos   GenClock   ClockSynchInst   Heard_Of   Consensus_Refined   Abortable_Linearizable_Modules   Concurrent: ConcurrentGC   Online: List_Update  

Concurrency

FLP   Process Calculi: AODV   AWN   CCS   Pi_Calculus   Psi_Calculi   Encodability_Process_Calculi   Circus  

Data Structures

List_Interleaving   Refine_Imperative_HOL   Amortized_Complexity   Dynamic_Tables   AVL-Trees   BDD   BinarySearchTree   Splay_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   Word_Lib  

Functional Programming

Show   Certification_Monads   Partial_Function_MR   Lifting_Definition_Option   Coinductive   Stream-Fusion   Tycon   XML   Tail_Recursive_Functions   Stream_Fusion_Code   Applicative_Lifting  

Games

Parity_Game  

Networks

IP_Addresses   Simple_Firewall   Iptables_Semantics   Routing  

Programming Languages

Language Definitions: pGCL   GPU_Kernel_PL   LightweightJava   CoreC++   FeatherweightJava   Jinja   JinjaThreads   Locally-Nameless-Sigma   AutoFocus-Stream   FocusStreamsCaseStudies   Isabelle_Meta_Model   Simpl   Lambda Calculi: Launchbury   PCF   POPLmark-deBruijn   Lam-ml-Normalization   Type Systems: 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   Compiling: Compiling-Exceptions-Correctly   NormByEval   Density_Compiler   Static Analysis: RIPEMD-160-SPARK   Program-Conflict-Analysis   Shivers-CFA   Slicing   HRB-Slicing   InfPathElimination   Transformations: Call_Arity   Refine_Imperative_HOL   WorkerWrapper   Formal_SSA   Misc: JiveDataStoreModel   Pop_Refinement   Case_Labeling  

System Description Languages

Circus   ComponentDependencies   Promela   Featherweight_OCL  

Security

Noninterference_Generic_Unwinding   Noninterference_Ipurge_Unwinding   UPF   CISC-Kernel   Noninterference_CSP   Inductive_Confidentiality   Possibilistic_Noninterference   SIFUM_Type_Systems   Dependent_SIFUM_Type_Systems   Dependent_SIFUM_Refinement   Strong_Security   WHATandWHERE_Security   VolpanoSmith   SIFPL   HotelKeyCards   RSAPSS   InformationFlowSlicing   InformationFlowSlicing_Inter   CryptoBasedCompositionalProperties   Probabilistic_Noninterference   HyperCTL   Bounded_Deducibility_Security   Network_Security_Policy_Verification   Noninterference_Inductive_Unwinding   Noninterference_Sequential_Composition   Noninterference_Concurrent_Composition  

Logic

MSO_Regex_Equivalence   Formula_Derivatives   Boolean_Expression_Checkers   Presburger-Automata   Verified-Prover   Completeness   Ordinal   Ordinals_and_Cardinals   FOL-Fitting   SequentInvertibility   LinearQuantifierElim   Nat-Interval-Logic   Recursion-Theory-I   Free-Boolean-Algebra   Sort_Encodings   LTL   HereditarilyFinite   Incompleteness   GoedelGod   HyperCTL   Abstract_Completeness   PropResPI   SuperCalc   Incredible_Proof_Machine   Resolution_FOL   Surprise_Paradox  

Rewriting

Abstract-Rewriting   Decreasing-Diagrams   Decreasing-Diagrams-II   Rewriting_Z  

Mathematics

Algebra

Buildings   Algebraic_VCs   Multirelations   Residuated_Lattices   PseudoHoops   LatticeProperties   Impossible_Geometry   Gauss-Jordan-Elim-Fun   Matrix_Tensor   Stone_Algebras   Kleene_Algebra   KAT_and_DRA   KAD   Regular_Algebras   Free-Groups   CofGroups   Group-Ring-Module   Robbins-Conjecture   Valuation   Rank_Nullity_Theorem   Relation_Algebra   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   Groebner_Bases   Multivariate_Polynomials  

Analysis

Liouville_Numbers   Descartes_Sign_Rule   Real_Impl   Lower_Semicontinuous   Affine_Arithmetic   Cauchy   Integration   Ordinary_Differential_Equations   Polynomials   Sqrt_Babylonian   Sturm_Sequences   Sturm_Tarski   Special_Function_Bounds   Landau_Symbols   Akra_Bazzi   Cartan_FP   Stirling_Formula  

Probability Theory

Markov_Models   Density_Compiler   Random_Graph_Subgraph_Threshold   Ergodic_Theory  

Number Theory

Prime_Harmonic_Series   Fermat3_4   Perfect-Number-Thm   SumSquares   Lehmer   Pratt_Certificate   Stern_Brocot  

Economics

ArrowImpossibilityGS   SenSocialChoice   Vickrey_Clarke_Groves   Randomised_Social_Choice   SDS_Impossibility  

Geometry

Buildings   Triangle   Impossible_Geometry   Tarskis_Geometry   General-Triangle   Ptolemys_Theorem  

Topology

Topology   Knot_Theory  

Graph Theory

MFMC_Countable   ShortestPath   Gabow_SCC   Graph_Theory   Planarity_Certificates   Max-Card-Matching   Girth_Chromatic   Random_Graph_Subgraph_Threshold   Flyspeck-Tame   Koenigsberg_Friendship   Tree_Decomposition  

Combinatorics

Card_Equiv_Relations   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  

Category Theory

Category3   Category   Category2  

Physics

No_FTL_observers  

Misc

FunWithFunctions   FunWithTilings  

Tools

Case_Labeling   DPT-SAT-Solver   Nominal2