Diffusion afp-devel ea64af8304a7

merge from afp-2020
ea64af8304a7
Actions

Tags

None

Subscribers

None

Description

merge from afp-2020

Details

Provenance

Authored on

Parents

rAFP91f1cdbeefc0: AFP-2020 website
rAFP7fc86009bce1: Added proofs for various properties of well-founded heaps and normalized type…

Branches

Unknown

Tags

Unknown

Event Timeline

kleing committed rAFPea64af8304a7: merge from afp-2020.Apr 21 2020, 3:17 AM

Merged Changes

7fc86009bce1 Added proofs for various properties of well-founded heaps and normalized type…
Author
Achim D. Brucker <adbrucker@0x5f.org>
Browse Repository
No Builds
No Audits
8f6e1822c2b8 Fixed typo.
Author
Achim D. Brucker <adbrucker@0x5f.org>
Browse Repository
No Builds
No Audits
27cde0ee0923 Refactoring: directory layout.
Author
Achim D. Brucker <adbrucker@0x5f.org>
Browse Repository
No Builds
No Audits
be8df5368af1 Fix missing files.
Author
Martin Rau
Browse Repository
No Builds
No Audits
7e54c722a284 Update KD_Tree entry to incorporate HOL-Analysis primites 'vec', 'dist' and…
Author
Martin Rau
Browse Repository
No Builds
No Audits
de0ced664a16 incorporate Time_Monad from AFP entry Root_Balanced_Tree; update proofs
Author
Martin Rau
Browse Repository
No Builds
No Audits
5978c17604c0 merge from afp-2020
Author
kleing
Browse Repository
No Builds
No Audits
9a2a0d63ca30 fixed a frac_le proof
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
eea502832a73 fixed a failing frac_le proof
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
ddaf86ffa226 merged
Author
Julian Brunner <julianbrunner@gmail.com>
Browse Repository
No Builds
No Audits
744b282fd492 updated benchmarks
Author
Julian Brunner <julianbrunner@gmail.com>
Browse Repository
No Builds
No Audits
819a553f7508 using proper atomic propositions, added more benchmarks
Author
Julian Brunner <julianbrunner@gmail.com>
Browse Repository
No Builds
No Audits
bde08698d726 avoid nonterminal clash in syntax translation
Author
traytel
Browse Repository
No Builds
No Audits
a0d561998f20 closed branch
Author
kleing
Browse Repository
No Builds
No Audits
8e995d947fb0 closed pull-request branch
Author
Gerwin Klein <gerwin.klein@nicta.com.au>
Browse Repository
No Builds
No Audits
249c2b58d173 closed merged branch
Author
Gerwin Klein <gerwin.klein@nicta.com.au>
Browse Repository
No Builds
No Audits
ad14484777fc merged
Author
gerwin.klein@nicta.com.au
Browse Repository
No Builds
No Audits
e3e858bfc9eb merged
Author
kleing
Browse Repository
No Builds
No Audits
4bea345493dd Closed branch ltl
Author
Salomon Sickert <sickert@in.tum.de>
Browse Repository
No Builds
No Audits
53421953ad96 WIP/LTL Entry
Author
Salomon Sickert <sickert@in.tum.de>
Browse Repository
No Builds
No Audits

Changes (532)
Show All Changes

Very Large Commit

This commit is very large. Load each file individually.

Path

Size

metadata/

thys/

Lambda_Free_RPOs/

Word_Lib/

Word_Lemmas.thy

web/

entries/

Abortable_Linearizable_Modules.html

Abs_Int_ITP2012.html

Abstract-Hoare-Logics.html

Abstract-Rewriting.html

Abstract_Completeness.html

Abstract_Soundness.html

Adaptive_State_Counting.html

Affine_Arithmetic.html

Aggregation_Algebras.html

Akra_Bazzi.html

Algebraic_Numbers.html

Algebraic_VCs.html

Allen_Calculus.html

Amortized_Complexity.html

Applicative_Lifting.html

Approximation_Algorithms.html

Architectural_Design_Patterns.html

Aristotles_Assertoric_Syllogistic.html

Arith_Prog_Rel_Primes.html

ArrowImpossibilityGS.html

Auto2_Imperative_HOL.html

AutoFocus-Stream.html

Automatic_Refinement.html

AxiomaticCategoryTheory.html

BNF_Operations.html

Bell_Numbers_Spivey.html

Berlekamp_Zassenhaus.html

Bertrands_Postulate.html

Bicategory.html

BinarySearchTree.html

Binding_Syntax_Theory.html

Binomial-Heaps.html

Binomial-Queues.html

Boolean_Expression_Checkers.html

Bounded_Deducibility_Security.html

Buchi_Complementation.html

Budan_Fourier.html

Buffons_Needle.html

BytecodeLogicJmlTypes.html

C2KA_DistributedSystems.html

CAVA_Automata.html

CAVA_LTL_Modelchecker.html

CISC-Kernel.html

CakeML_Codegen.html

Call_Arity.html

Card_Equiv_Relations.html

Card_Multisets.html

Card_Number_Partitions.html

Card_Partitions.html

Case_Labeling.html

Catalan_Numbers.html

Cayley_Hamilton.html

Certification_Monads.html

Chord_Segments.html

ClockSynchInst.html

Closest_Pair_Points.html

Coinductive.html

Coinductive_Languages.html

Collections.html

Comparison_Sort_Lower_Bound.html

Compiling-Exceptions-Correctly.html

Complete_Non_Orders.html

Completeness.html

Complex_Geometry.html

ComponentDependencies.html

ConcurrentGC.html

ConcurrentIMP.html

Concurrent_Ref_Alg.html

Concurrent_Revisions.html

Consensus_Refined.html

Constructive_Cryptography.html

Constructor_Funs.html

Containers.html

Count_Complex_Roots.html

CryptoBasedCompositionalProperties.html

DFS_Framework.html

DPT-SAT-Solver.html

DataRefinementIBP.html

Datatype_Order_Generator.html

Decl_Sem_Fun_PL.html

Decreasing-Diagrams-II.html

Decreasing-Diagrams.html

Deep_Learning.html

Density_Compiler.html

Dependent_SIFUM_Refinement.html

Dependent_SIFUM_Type_Systems.html

Depth-First-Search.html

Derangements.html

Descartes_Sign_Rule.html

Dict_Construction.html

Differential_Dynamic_Logic.html

Differential_Game_Logic.html

Dijkstra_Shortest_Path.html

Diophantine_Eqns_Lin_Hom.html

Dirichlet_L.html

Dirichlet_Series.html

DiscretePricing.html

Discrete_Summation.html

DynamicArchitectures.html

Dynamic_Tables.html

E_Transcendental.html

Echelon_Form.html

EdmondsKarp_Maxflow.html

Efficient-Mergesort.html

Elliptic_Curves_Group_Law.html

Encodability_Process_Calculi.html

Epistemic_Logic.html

Ergodic_Theory.html

Error_Function.html

Euler_MacLaurin.html

Euler_Partition.html

FOL-Fitting.html

FOL_Harrison.html

FOL_Seq_Calc1.html

Factored_Transition_System_Bounding.html

Falling_Factorial_Sum.html

FeatherweightJava.html

Featherweight_OCL.html

FileRefinement.html

Finger-Trees.html

Finite_Automata_HF.html

First_Order_Terms.html

First_Welfare_Theorem.html

Fishburn_Impossibility.html

Fisher_Yates.html

Flow_Networks.html

Floyd_Warshall.html

Flyspeck-Tame.html

FocusStreamsCaseStudies.html

Formal_SSA.html

Formula_Derivatives.html

Free-Boolean-Algebra.html

Free-Groups.html

FunWithFunctions.html

FunWithTilings.html

Functional-Automata.html

Functional_Ordered_Resolution_Prover.html

Furstenberg_Topology.html

GPU_Kernel_PL.html

Game_Based_Crypto.html

Gauss-Jordan-Elim-Fun.html

Gauss_Jordan.html

Gauss_Sums.html

General-Triangle.html

Generalized_Counting_Sort.html

Generic_Deriving.html

Generic_Join.html

GewirthPGCProof.html

Girth_Chromatic.html

Goodstein_Lambda.html

GraphMarkingIBP.html

Graph_Saturation.html

Graph_Theory.html

Groebner_Bases.html

Groebner_Macaulay.html

Gromov_Hyperbolicity.html

Group-Ring-Module.html

HOLCF-Prelude.html

HRB-Slicing.html

Hello_World.html

HereditarilyFinite.html

Hidden_Markov_Models.html

Higher_Order_Terms.html

Hoare_Time.html

HotelKeyCards.html

Hybrid_Logic.html

Hybrid_Multi_Lane_Spatial_Logic.html

Hybrid_Systems_VCs.html

IEEE_Floating_Point.html

IMP2_Binary_Heap.html

IP_Addresses.html

Imperative_Insertion_Sort.html

Impossible_Geometry.html

Incompleteness.html

Incredible_Proof_Machine.html

Inductive_Confidentiality.html

InfPathElimination.html

InformationFlowSlicing.html

InformationFlowSlicing_Inter.html

Integration.html

Interval_Arithmetic_Word32.html

Iptables_Semantics.html

Irrationality_J_Hancl.html

Isabelle_C.html

Isabelle_Meta_Model.html

Jacobson_Basic_Algebra.html

JinjaThreads.html

JiveDataStoreModel.html

Jordan_Hoelder.html

Jordan_Normal_Form.html

KAT_and_DRA.html

Key_Agreement_Strong_Adversaries.html

Kleene_Algebra.html

Knot_Theory.html

Knuth_Morris_Pratt.html

Koenigsberg_Friendship.html

Kuratowski_Closure_Complement.html

LLL_Basis_Reduction.html

LLL_Factorization.html

LTL_Master_Theorem.html

LTL_to_DRA.html

LTL_to_GBA.html

Lam-ml-Normalization.html

LambdaAuth.html

Lambda_Free_EPO.html

Lambda_Free_KBOs.html

Lambda_Free_RPOs.html

Landau_Symbols.html

Laplace_Transform.html

Latin_Square.html

LatticeProperties.html

Launchbury.html

Lazy-Lists-II.html

Lifting_Definition_Option.html

LightweightJava.html

LinearQuantifierElim.html

Linear_Inequalities.html

Linear_Programming.html

Linear_Recurrences.html

Liouville_Numbers.html

List-Index.html

List-Infinite.html

List_Interleaving.html

List_Inversions.html

List_Update.html

LocalLexing.html

Localization_Ring.html

Locally-Nameless-Sigma.html

Lowe_Ontological_Argument.html

Lower_Semicontinuous.html

MFMC_Countable.html

MFODL_Monitor_Optimized.html

MFOTL_Monitor.html

MSO_Regex_Equivalence.html

Markov_Models.html

Mason_Stothers.html

Matrix_Tensor.html

Max-Card-Matching.html

Median_Of_Medians_Selection.html

Mersenne_Primes.html

Minimal_SSA.html

Minkowskis_Theorem.html

Minsky_Machines.html

Modal_Logics_for_NTS.html

Modular_Assembly_Kit_Security.html

Monad_Memo_DP.html

Monad_Normalisation.html

MonoBoolTranAlgebra.html

MonoidalCategory.html

Monomorphic_Monad.html

MuchAdoAboutTwo.html

Multi_Party_Computation.html

Multirelations.html

Myhill-Nerode.html

Name_Carrying_Type_Inference.html

Nat-Interval-Logic.html

Native_Word.html

Nested_Multisets_Ordinals.html

Network_Security_Policy_Verification.html

Neumann_Morgenstern_Utility.html

No_FTL_observers.html

Noninterference_CSP.html

Noninterference_Concurrent_Composition.html

Noninterference_Generic_Unwinding.html

Noninterference_Inductive_Unwinding.html

Noninterference_Ipurge_Unwinding.html

Noninterference_Sequential_Composition.html

NormByEval.html

Nullstellensatz.html

Open_Induction.html

Optimal_BST.html

Orbit_Stabiliser.html

Order_Lattice_Props.html

Ordered_Resolution_Prover.html

Ordinals_and_Cardinals.html

Ordinary_Differential_Equations.html

POPLmark-deBruijn.html

PSemigroupsConvolution.html

Pairing_Heap.html

Paraconsistency.html

Parity_Game.html

Partial_Function_MR.html

Partial_Order_Reduction.html

Password_Authentication_Protocol.html

Perfect-Number-Thm.html

Perron_Frobenius.html

Pi_Calculus.html

Pi_Transcendental.html

Planarity_Certificates.html

Poincare_Bendixson.html

Poincare_Disc.html

Polynomial_Factorization.html

Polynomial_Interpolation.html

Polynomials.html

Pop_Refinement.html

Posix-Lexing.html

Possibilistic_Noninterference.html

Pratt_Certificate.html

Presburger-Automata.html

Prim_Dijkstra_Simple.html

Prime_Distribution_Elementary.html

Prime_Harmonic_Series.html

Prime_Number_Theorem.html

Priority_Queue_Braun.html

Priority_Search_Trees.html

Probabilistic_Noninterference.html

Probabilistic_Prime_Tests.html

Probabilistic_System_Zoo.html

Probabilistic_Timed_Automata.html

Probabilistic_While.html

Program-Conflict-Analysis.html

Projective_Geometry.html

Proof_Strategy_Language.html

Propositional_Proof_Systems.html

Prpu_Maxflow.html

PseudoHoops.html

Psi_Calculi.html

Ptolemys_Theorem.html

QR_Decomposition.html

Quaternions.html

Quick_Sort_Cost.html

RIPEMD-160-SPARK.html

Ramsey-Infinite.html

Random_BSTs.html

Random_Graph_Subgraph_Threshold.html

Randomised_BSTs.html

Randomised_Social_Choice.html

Rank_Nullity_Theorem.html

Recursion-Theory-I.html

Refine_Imperative_HOL.html

Refine_Monadic.html

RefinementReactive.html

Regex_Equivalence.html

Regular-Sets.html

Regular_Algebras.html

Relation_Algebra.html

Relational-Incorrectness-Logic.html

Rep_Fin_Groups.html

Residuated_Lattices.html

Resolution_FOL.html

Rewriting_Z.html

Ribbon_Proofs.html

Robbins-Conjecture.html

Root_Balanced_Tree.html

Roy_Floyd_Warshall.html

SATSolverVerification.html

SDS_Impossibility.html

SIFUM_Type_Systems.html

Saturation_Framework.html

Secondary_Sylow.html

Security_Protocol_Refinement.html

Selection_Heap_Sort.html

SenSocialChoice.html

Separation_Algebra.html

Separation_Logic_Imperative_HOL.html

SequentInvertibility.html

Shivers-CFA.html

ShortestPath.html

Sigma_Commit_Crypto.html

Signature_Groebner.html

Simple_Firewall.html

Skip_Lists.html

Sliding_Window_Algorithm.html

Smooth_Manifolds.html

Sort_Encodings.html

Source_Coding_Theorem.html

Special_Function_Bounds.html

Splay_Tree.html

Sqrt_Babylonian.html

Stable_Matching.html

Statecharts.html

Stellar_Quorums.html

Stern_Brocot.html

Stewart_Apollonius.html

Stirling_Formula.html

Stochastic_Matrices.html

Stone_Algebras.html

Stone_Kleene_Relation_Algebras.html

Stone_Relation_Algebras.html

Store_Buffer_Reduction.html

Stream-Fusion.html

Stream_Fusion_Code.html

Strong_Security.html

Sturm_Sequences.html

Sturm_Tarski.html

Stuttering_Equivalence.html

Subresultants.html

Subset_Boolean_Algebras.html

SumSquares.html

Surprise_Paradox.html

Symmetric_Polynomials.html

TESL_Language.html

Tail_Recursive_Functions.html

Tarskis_Geometry.html

Taylor_Models.html

Timed_Automata.html

TortoiseHare.html

Transcendence_Series_Hancl_Rucki.html

Transformer_Semantics.html

Transition_Systems_and_Automata.html

Transitive-Closure-II.html

Transitive-Closure.html

Tree-Automata.html

Tree_Decomposition.html

Twelvefold_Way.html

Types_Tableaus_and_Goedels_God.html

UPF_Firewall.html

Universal_Turing_Machine.html

UpDown_Scheme.html

VectorSpace.html

Verified-Prover.html

VerifyThis2018.html

VerifyThis2019.html

Vickrey_Clarke_Groves.html

VolpanoSmith.html

WHATandWHERE_Security.html

WOOT_Strong_Eventual_Consistency.html

WebAssembly.html

Weight_Balanced_Trees.html

Well_Quasi_Orders.html

Winding_Number_Eval.html

WorkerWrapper.html

ZFC_in_HOL.html

Zeta_3_Irrational.html

Zeta_Function.html

statistics.html

rAFPea64af8304a7

metadata/release-dates

metadata/releases

thys/Lambda_Free_RPOs/ROOT

thys/Word_Lib/Word_Lemmas.thy

web/entries/AODV.html

web/entries/AVL-Trees.html

web/entries/AWN.html

web/entries/Abortable_Linearizable_Modules.html

web/entries/Abs_Int_ITP2012.html

web/entries/Abstract-Hoare-Logics.html

web/entries/Abstract-Rewriting.html

web/entries/Abstract_Completeness.html

web/entries/Abstract_Soundness.html

web/entries/Adaptive_State_Counting.html

web/entries/Affine_Arithmetic.html

web/entries/Aggregation_Algebras.html

web/entries/Akra_Bazzi.html

web/entries/Algebraic_Numbers.html

web/entries/Algebraic_VCs.html

web/entries/Allen_Calculus.html

web/entries/Amortized_Complexity.html

web/entries/AnselmGod.html

web/entries/Applicative_Lifting.html

web/entries/Approximation_Algorithms.html

web/entries/Architectural_Design_Patterns.html

web/entries/Aristotles_Assertoric_Syllogistic.html

web/entries/Arith_Prog_Rel_Primes.html

web/entries/ArrowImpossibilityGS.html

web/entries/Auto2_HOL.html

web/entries/Auto2_Imperative_HOL.html

web/entries/AutoFocus-Stream.html

web/entries/Automatic_Refinement.html

web/entries/AxiomaticCategoryTheory.html

web/entries/BDD.html

web/entries/BNF_CC.html

web/entries/BNF_Operations.html

web/entries/Bell_Numbers_Spivey.html

web/entries/Berlekamp_Zassenhaus.html

web/entries/Bernoulli.html

web/entries/Bertrands_Postulate.html

web/entries/Bicategory.html

web/entries/BinarySearchTree.html

web/entries/Binding_Syntax_Theory.html

web/entries/Binomial-Heaps.html

web/entries/Binomial-Queues.html

web/entries/Bondy.html

web/entries/Boolean_Expression_Checkers.html

web/entries/Bounded_Deducibility_Security.html

web/entries/Buchi_Complementation.html

web/entries/Budan_Fourier.html

web/entries/Buffons_Needle.html

web/entries/Buildings.html

web/entries/BytecodeLogicJmlTypes.html

web/entries/C2KA_DistributedSystems.html

web/entries/CAVA_Automata.html

web/entries/CAVA_LTL_Modelchecker.html

web/entries/CCS.html

web/entries/CISC-Kernel.html

web/entries/CRDT.html

web/entries/CYK.html

web/entries/CakeML.html

web/entries/CakeML_Codegen.html

web/entries/Call_Arity.html

web/entries/Card_Equiv_Relations.html

web/entries/Card_Multisets.html

web/entries/Card_Number_Partitions.html

web/entries/Card_Partitions.html

web/entries/Cartan_FP.html

web/entries/Case_Labeling.html

web/entries/Catalan_Numbers.html

web/entries/Category.html

web/entries/Category2.html

web/entries/Category3.html

web/entries/Cauchy.html

web/entries/Cayley_Hamilton.html

web/entries/Certification_Monads.html

web/entries/Chord_Segments.html

web/entries/Circus.html

web/entries/Clean.html

web/entries/ClockSynchInst.html

web/entries/Closest_Pair_Points.html

web/entries/CofGroups.html

web/entries/Coinductive.html

web/entries/Coinductive_Languages.html

web/entries/Collections.html

web/entries/Comparison_Sort_Lower_Bound.html

web/entries/Compiling-Exceptions-Correctly.html

web/entries/Complete_Non_Orders.html

web/entries/Completeness.html

web/entries/Complex_Geometry.html

web/entries/Complx.html

web/entries/ComponentDependencies.html

web/entries/ConcurrentGC.html

web/entries/ConcurrentIMP.html

web/entries/Concurrent_Ref_Alg.html

web/entries/Concurrent_Revisions.html

web/entries/Consensus_Refined.html

web/entries/Constructive_Cryptography.html

web/entries/Constructor_Funs.html

web/entries/Containers.html

web/entries/CoreC++.html

web/entries/Core_DOM.html

web/entries/Count_Complex_Roots.html

web/entries/CryptHOL.html

web/entries/CryptoBasedCompositionalProperties.html

web/entries/DFS_Framework.html

web/entries/DPT-SAT-Solver.html

web/entries/DataRefinementIBP.html

web/entries/Datatype_Order_Generator.html

web/entries/Decl_Sem_Fun_PL.html

web/entries/Decreasing-Diagrams-II.html

web/entries/Decreasing-Diagrams.html

web/entries/Deep_Learning.html

web/entries/Density_Compiler.html

web/entries/Dependent_SIFUM_Refinement.html

web/entries/Dependent_SIFUM_Type_Systems.html

web/entries/Depth-First-Search.html

web/entries/Derangements.html

web/entries/Deriving.html

web/entries/Descartes_Sign_Rule.html

web/entries/Dict_Construction.html

web/entries/Differential_Dynamic_Logic.html

web/entries/Differential_Game_Logic.html

web/entries/Dijkstra_Shortest_Path.html

web/entries/Diophantine_Eqns_Lin_Hom.html

web/entries/Dirichlet_L.html

web/entries/Dirichlet_Series.html

web/entries/DiscretePricing.html

web/entries/Discrete_Summation.html

web/entries/DiskPaxos.html

web/entries/DynamicArchitectures.html

web/entries/Dynamic_Tables.html

web/entries/E_Transcendental.html

web/entries/Echelon_Form.html

web/entries/EdmondsKarp_Maxflow.html

web/entries/Efficient-Mergesort.html

web/entries/Elliptic_Curves_Group_Law.html

web/entries/Encodability_Process_Calculi.html

web/entries/Epistemic_Logic.html

web/entries/Ergodic_Theory.html

web/entries/Error_Function.html

web/entries/Euler_MacLaurin.html

web/entries/Euler_Partition.html

web/entries/FFT.html

web/entries/FLP.html

web/entries/FOL-Fitting.html

web/entries/FOL_Harrison.html

web/entries/FOL_Seq_Calc1.html

web/entries/Factored_Transition_System_Bounding.html

web/entries/Falling_Factorial_Sum.html

web/entries/Farkas.html

web/entries/FeatherweightJava.html

web/entries/Featherweight_OCL.html

web/entries/Fermat3_4.html

web/entries/FileRefinement.html

web/entries/FinFun.html

web/entries/Finger-Trees.html

web/entries/Finite_Automata_HF.html

web/entries/First_Order_Terms.html

web/entries/First_Welfare_Theorem.html

web/entries/Fishburn_Impossibility.html

web/entries/Fisher_Yates.html

web/entries/Flow_Networks.html

web/entries/Floyd_Warshall.html

web/entries/Flyspeck-Tame.html

web/entries/FocusStreamsCaseStudies.html

web/entries/Formal_SSA.html

web/entries/Formula_Derivatives.html

web/entries/Fourier.html

web/entries/Free-Boolean-Algebra.html

web/entries/Free-Groups.html

web/entries/FunWithFunctions.html

web/entries/FunWithTilings.html

web/entries/Functional-Automata.html

web/entries/Functional_Ordered_Resolution_Prover.html

web/entries/Furstenberg_Topology.html

web/entries/GPU_Kernel_PL.html

web/entries/Gabow_SCC.html

web/entries/Game_Based_Crypto.html

web/entries/Gauss-Jordan-Elim-Fun.html

web/entries/Gauss_Jordan.html

web/entries/Gauss_Sums.html

web/entries/GenClock.html

web/entries/General-Triangle.html

web/entries/Generalized_Counting_Sort.html

web/entries/Generic_Deriving.html

web/entries/Generic_Join.html

web/entries/GewirthPGCProof.html

web/entries/Girth_Chromatic.html

web/entries/GoedelGod.html

web/entries/Goodstein_Lambda.html

web/entries/GraphMarkingIBP.html

web/entries/Graph_Saturation.html

web/entries/Graph_Theory.html

web/entries/Green.html

web/entries/Groebner_Bases.html

web/entries/Groebner_Macaulay.html

web/entries/Gromov_Hyperbolicity.html

web/entries/Group-Ring-Module.html

web/entries/HOL-CSP.html

web/entries/HOLCF-Prelude.html

web/entries/HRB-Slicing.html

web/entries/Heard_Of.html

web/entries/Hello_World.html

web/entries/HereditarilyFinite.html

web/entries/Hermite.html

web/entries/Hidden_Markov_Models.html

web/entries/Higher_Order_Terms.html

web/entries/Hoare_Time.html

web/entries/HotelKeyCards.html

web/entries/Huffman.html

web/entries/Hybrid_Logic.html

web/entries/Hybrid_Multi_Lane_Spatial_Logic.html

web/entries/Hybrid_Systems_VCs.html

web/entries/HyperCTL.html

web/entries/IEEE_Floating_Point.html

web/entries/IMAP-CRDT.html

web/entries/IMO2019.html

web/entries/IMP2.html

web/entries/IMP2_Binary_Heap.html

web/entries/IP_Addresses.html

web/entries/Imperative_Insertion_Sort.html

web/entries/Impossible_Geometry.html

web/entries/Incompleteness.html

web/entries/Incredible_Proof_Machine.html

web/entries/Inductive_Confidentiality.html

web/entries/InfPathElimination.html

web/entries/InformationFlowSlicing.html

web/entries/InformationFlowSlicing_Inter.html

web/entries/Integration.html

web/entries/Interval_Arithmetic_Word32.html

web/entries/Iptables_Semantics.html

web/entries/Irrationality_J_Hancl.html

web/entries/Isabelle_C.html

web/entries/Isabelle_Meta_Model.html

web/entries/Jacobson_Basic_Algebra.html

web/entries/Jinja.html

web/entries/JinjaThreads.html

web/entries/JiveDataStoreModel.html

web/entries/Jordan_Hoelder.html

web/entries/Jordan_Normal_Form.html

web/entries/KAD.html

web/entries/KAT_and_DRA.html

web/entries/KBPs.html

web/entries/KD_Tree.html

web/entries/Key_Agreement_Strong_Adversaries.html

web/entries/Kleene_Algebra.html

web/entries/Knot_Theory.html

web/entries/Knuth_Morris_Pratt.html

web/entries/Koenigsberg_Friendship.html

web/entries/Kruskal.html

web/entries/Kuratowski_Closure_Complement.html

web/entries/LLL_Basis_Reduction.html

web/entries/LLL_Factorization.html

web/entries/LOFT.html

web/entries/LTL.html

web/entries/LTL_Master_Theorem.html

web/entries/LTL_to_DRA.html

web/entries/LTL_to_GBA.html

web/entries/Lam-ml-Normalization.html

web/entries/LambdaAuth.html

web/entries/LambdaMu.html

web/entries/Lambda_Free_EPO.html

web/entries/Lambda_Free_KBOs.html

web/entries/Lambda_Free_RPOs.html

web/entries/Landau_Symbols.html

web/entries/Laplace_Transform.html

web/entries/Latin_Square.html

web/entries/LatticeProperties.html

web/entries/Launchbury.html

web/entries/Lazy-Lists-II.html

web/entries/Lazy_Case.html

web/entries/Lehmer.html

web/entries/Lifting_Definition_Option.html

web/entries/LightweightJava.html

web/entries/LinearQuantifierElim.html

web/entries/Linear_Inequalities.html

web/entries/Linear_Programming.html

web/entries/Linear_Recurrences.html

web/entries/Liouville_Numbers.html

web/entries/List-Index.html

web/entries/List-Infinite.html

web/entries/List_Interleaving.html

web/entries/List_Inversions.html

web/entries/List_Update.html

web/entries/LocalLexing.html

web/entries/Localization_Ring.html

web/entries/Locally-Nameless-Sigma.html

web/entries/Lowe_Ontological_Argument.html

web/entries/Lower_Semicontinuous.html

web/entries/Lp.html

web/entries/MFMC_Countable.html

web/entries/MFODL_Monitor_Optimized.html

web/entries/MFOTL_Monitor.html

web/entries/MSO_Regex_Equivalence.html

web/entries/Markov_Models.html

web/entries/Marriage.html

web/entries/Mason_Stothers.html

web/entries/Matrix.html

web/entries/Matrix_Tensor.html

web/entries/Matroids.html

web/entries/Max-Card-Matching.html

web/entries/Median_Of_Medians_Selection.html

web/entries/Menger.html

web/entries/Mersenne_Primes.html

web/entries/MiniML.html

web/entries/Minimal_SSA.html

web/entries/Minkowskis_Theorem.html

web/entries/Minsky_Machines.html

web/entries/Modal_Logics_for_NTS.html

web/entries/Modular_Assembly_Kit_Security.html

web/entries/Monad_Memo_DP.html

web/entries/Monad_Normalisation.html

web/entries/MonoBoolTranAlgebra.html

web/entries/MonoidalCategory.html

web/entries/Monomorphic_Monad.html

web/entries/MuchAdoAboutTwo.html

web/entries/Multi_Party_Computation.html

web/entries/Multirelations.html

web/entries/Myhill-Nerode.html

web/entries/Name_Carrying_Type_Inference.html

web/entries/Nat-Interval-Logic.html

web/entries/Native_Word.html

web/entries/Nested_Multisets_Ordinals.html

web/entries/Network_Security_Policy_Verification.html

web/entries/Neumann_Morgenstern_Utility.html

web/entries/No_FTL_observers.html

web/entries/Nominal2.html

web/entries/Noninterference_CSP.html

web/entries/Noninterference_Concurrent_Composition.html

web/entries/Noninterference_Generic_Unwinding.html

web/entries/Noninterference_Inductive_Unwinding.html

web/entries/Noninterference_Ipurge_Unwinding.html

web/entries/Noninterference_Sequential_Composition.html

web/entries/NormByEval.html

web/entries/Nullstellensatz.html

web/entries/Octonions.html

web/entries/OpSets.html

web/entries/Open_Induction.html

web/entries/Optics.html

web/entries/Optimal_BST.html

web/entries/Orbit_Stabiliser.html

web/entries/Order_Lattice_Props.html

web/entries/Ordered_Resolution_Prover.html

web/entries/Ordinal.html

web/entries/Ordinals_and_Cardinals.html

web/entries/Ordinary_Differential_Equations.html

web/entries/PCF.html

web/entries/PLM.html

web/entries/POPLmark-deBruijn.html

web/entries/PSemigroupsConvolution.html

web/entries/Pairing_Heap.html

web/entries/Paraconsistency.html

web/entries/Parity_Game.html

web/entries/Partial_Function_MR.html

web/entries/Partial_Order_Reduction.html

web/entries/Password_Authentication_Protocol.html

web/entries/Pell.html

web/entries/Perfect-Number-Thm.html

web/entries/Perron_Frobenius.html

web/entries/Pi_Calculus.html

web/entries/Pi_Transcendental.html

web/entries/Planarity_Certificates.html

web/entries/Poincare_Bendixson.html

web/entries/Poincare_Disc.html

web/entries/Polynomial_Factorization.html

web/entries/Polynomial_Interpolation.html

web/entries/Polynomials.html

web/entries/Pop_Refinement.html

web/entries/Posix-Lexing.html

web/entries/Possibilistic_Noninterference.html

web/entries/Pratt_Certificate.html

web/entries/Presburger-Automata.html

web/entries/Prim_Dijkstra_Simple.html

web/entries/Prime_Distribution_Elementary.html

web/entries/Prime_Harmonic_Series.html

web/entries/Prime_Number_Theorem.html

web/entries/Priority_Queue_Braun.html

web/entries/Priority_Search_Trees.html

web/entries/Probabilistic_Noninterference.html

web/entries/Probabilistic_Prime_Tests.html

web/entries/Probabilistic_System_Zoo.html

web/entries/Probabilistic_Timed_Automata.html

web/entries/Probabilistic_While.html

web/entries/Program-Conflict-Analysis.html

web/entries/Projective_Geometry.html

web/entries/Promela.html

web/entries/Proof_Strategy_Language.html

web/entries/PropResPI.html

web/entries/Propositional_Proof_Systems.html

web/entries/Prpu_Maxflow.html

web/entries/PseudoHoops.html

web/entries/Psi_Calculi.html

web/entries/Ptolemys_Theorem.html

web/entries/QHLProver.html

web/entries/QR_Decomposition.html

web/entries/Quantales.html

web/entries/Quaternions.html

web/entries/Quick_Sort_Cost.html

web/entries/RIPEMD-160-SPARK.html

web/entries/ROBDD.html

web/entries/RSAPSS.html

web/entries/Ramsey-Infinite.html

web/entries/Random_BSTs.html

web/entries/Random_Graph_Subgraph_Threshold.html

web/entries/Randomised_BSTs.html

web/entries/Randomised_Social_Choice.html

web/entries/Rank_Nullity_Theorem.html

web/entries/Real_Impl.html

web/entries/Recursion-Theory-I.html

web/entries/Refine_Imperative_HOL.html

web/entries/Refine_Monadic.html

web/entries/RefinementReactive.html

web/entries/Regex_Equivalence.html

web/entries/Regular-Sets.html

web/entries/Regular_Algebras.html

web/entries/Relation_Algebra.html

web/entries/Relational-Incorrectness-Logic.html

web/entries/Rep_Fin_Groups.html

web/entries/Residuated_Lattices.html

web/entries/Resolution_FOL.html

web/entries/Rewriting_Z.html

web/entries/Ribbon_Proofs.html

web/entries/Robbins-Conjecture.html

web/entries/Root_Balanced_Tree.html

web/entries/Routing.html

web/entries/Roy_Floyd_Warshall.html

web/entries/SATSolverVerification.html

web/entries/SDS_Impossibility.html

web/entries/SIFPL.html

web/entries/SIFUM_Type_Systems.html

web/entries/SPARCv8.html

web/entries/Safe_OCL.html

web/entries/Saturation_Framework.html

web/entries/Secondary_Sylow.html

web/entries/Security_Protocol_Refinement.html

web/entries/Selection_Heap_Sort.html

web/entries/SenSocialChoice.html

web/entries/Separata.html

web/entries/Separation_Algebra.html

web/entries/Separation_Logic_Imperative_HOL.html

web/entries/SequentInvertibility.html

web/entries/Shivers-CFA.html

web/entries/ShortestPath.html

web/entries/Show.html

web/entries/Sigma_Commit_Crypto.html

web/entries/Signature_Groebner.html

web/entries/Simpl.html

web/entries/Simple_Firewall.html

web/entries/Simplex.html

web/entries/Skew_Heap.html

web/entries/Skip_Lists.html

web/entries/Slicing.html

web/entries/Sliding_Window_Algorithm.html

web/entries/Smooth_Manifolds.html

web/entries/Sort_Encodings.html

web/entries/Source_Coding_Theorem.html

web/entries/Special_Function_Bounds.html

web/entries/Splay_Tree.html

web/entries/Sqrt_Babylonian.html

web/entries/Stable_Matching.html

web/entries/Statecharts.html

web/entries/Stellar_Quorums.html

web/entries/Stern_Brocot.html

web/entries/Stewart_Apollonius.html

web/entries/Stirling_Formula.html

web/entries/Stochastic_Matrices.html

web/entries/Stone_Algebras.html

web/entries/Stone_Kleene_Relation_Algebras.html

web/entries/Stone_Relation_Algebras.html

web/entries/Store_Buffer_Reduction.html

web/entries/Stream-Fusion.html

web/entries/Stream_Fusion_Code.html

web/entries/Strong_Security.html

web/entries/Sturm_Sequences.html

web/entries/Sturm_Tarski.html

web/entries/Stuttering_Equivalence.html

web/entries/Subresultants.html

web/entries/Subset_Boolean_Algebras.html

web/entries/SumSquares.html

web/entries/SuperCalc.html

web/entries/Surprise_Paradox.html

web/entries/Symmetric_Polynomials.html

web/entries/Szpilrajn.html

web/entries/TESL_Language.html

web/entries/TLA.html

web/entries/Tail_Recursive_Functions.html

web/entries/Tarskis_Geometry.html

web/entries/Taylor_Models.html

web/entries/Timed_Automata.html

web/entries/Topology.html

web/entries/TortoiseHare.html

web/entries/Transcendence_Series_Hancl_Rucki.html

web/entries/Transformer_Semantics.html

web/entries/Transition_Systems_and_Automata.html

web/entries/Transitive-Closure-II.html

web/entries/Transitive-Closure.html

web/entries/Treaps.html

web/entries/Tree-Automata.html

web/entries/Tree_Decomposition.html

web/entries/Triangle.html

web/entries/Trie.html

web/entries/Twelvefold_Way.html

web/entries/Tycon.html

web/entries/Types_Tableaus_and_Goedels_God.html

web/entries/UPF.html

web/entries/UPF_Firewall.html

web/entries/UTP.html

web/entries/Universal_Turing_Machine.html

web/entries/UpDown_Scheme.html

web/entries/Valuation.html

web/entries/VectorSpace.html

web/entries/VeriComp.html

web/entries/Verified-Prover.html

web/entries/VerifyThis2018.html

web/entries/VerifyThis2019.html

web/entries/Vickrey_Clarke_Groves.html

web/entries/VolpanoSmith.html

web/entries/WHATandWHERE_Security.html

web/entries/WOOT_Strong_Eventual_Consistency.html

web/entries/WebAssembly.html

web/entries/Weight_Balanced_Trees.html

web/entries/Well_Quasi_Orders.html

web/entries/Winding_Number_Eval.html

web/entries/Word_Lib.html

web/entries/WorkerWrapper.html

web/entries/XML.html

web/entries/ZFC_in_HOL.html

web/entries/Zeta_3_Irrational.html

web/entries/Zeta_Function.html

web/entries/pGCL.html

web/statistics.html