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
Artificial intelligence
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
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
Machine learning
Networks
Programming languages
Decl_Sem_Fun_PL
Clean
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
Cryptography | RSAPSS 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
General logic
Topological_Semantics
Metalogic_ProofChecker
Classical first-order logic | FOL-Fitting FOL_Axiomatic FOL_Seq_Calc2 Eval_FO FOL_Seq_Calc3 |
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 Blue_Eyes Public_Announcement_Logic Belief_Revision PAL |
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 FOL_Seq_Calc2 FOL_Seq_Calc3 |
Modal logic | Modal_Logics_for_NTS Differential_Dynamic_Logic Hybrid_Multi_Lane_Spatial_Logic Hybrid_Logic MFODL_Monitor_Optimized SimplifiedOntologicalArgument |
Paraconsistent logics | Paraconsistency |
Temporal logic | Nat-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
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
Physics
No_FTL_observers
Safe_Distance
Physical_Quantities
Schutz_Spacetime
Quantum information | Isabelle_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