_index.md (4979B)
1 +++ 2 title = "Logical Verification" 3 +++ 4 5 # Logical Verification 6 7 [This is the official website](https://lean-forward.github.io/logical-verification/2020/index.html). 8 There is a [Git repository](https://github.com/blanchette/logical_verification_2020) and a [book](https://github.com/blanchette/logical_verification_2020/raw/master/hitchhikers_guide.pdf) (also [formatted for tablets](https://github.com/blanchette/logical_verification_2020/raw/master/hitchhikers_guide_tablet.pdf)). 9 10 - [Basics](basics) 11 - [Type checking](basics#type-checking) 12 - [Lean diagnosis commands](basics#lean-diagnosis-commands) 13 - [Inductive type definitions](basics#inductive-type-definitions) 14 - [Function definitions](basics#function-definitions) 15 - [Backward proofs](backward-proofs) 16 - [Rewrite rules](backward-proofs#rewrite-rules) 17 - [Forward proofs](forward-proofs) 18 - [Structured constructs](forward-proofs#structured-constructs) 19 - [Calculational proofs](forward-proofs#calculational-proofs) 20 - [Dependent types](forward-proofs#dependent-types) 21 - [Curry-Howard Correspondence](forward-proofs#curry-howard-correspondence) 22 - [Induction by pattern matching](forward-proofs#induction-by-pattern-matching) 23 - [Functional programming](functional-programming) 24 - [Inductive types](functional-programming#inductive-types) 25 - [Structural induction](functional-programming#structural-induction) 26 - [Structural recursion](functional-programming#structural-recursion) 27 - [Pattern matching](functional-programming#pattern-matching) 28 - [Structures](functional-programming#structures) 29 - [Type classes](functional-programming#type-classes) 30 - [Lists](functional-programming#lists) 31 - [Binary trees](functional-programming#binary-trees) 32 - [Inductive predicates](inductive-predicates) 33 - [Monads](monads) 34 - [Two operations, three laws](monads#two-operations-three-laws) 35 - [Mutable state](monads#mutable-state) 36 - [Nondeterminism](monads#nondeterminism) 37 - [Metaprogramming](metaprogramming) 38 - [Tactics, tactic combinators](metaprogramming#tactics-tactic-combinators) 39 - [The metaprogramming monad](metaprogramming#the-metaprogramming-monad) 40 - [Operational semantics](operational-semantics) 41 - [Creating a small imperative language: WHILE](operational-semantics#creating-a-small-imperative-language-while) 42 - [Big-step (natural) semantics](operational-semantics#big-step-natural-semantics) 43 - [Properties of big-step semantics](operational-semantics#properties-of-big-step-semantics) 44 - [Small-step semantics](operational-semantics#small-step-semantics) 45 - [Properties of small-step semantics](operational-semantics#properties-of-small-step-semantics) 46 - [Hoare logic](hoare-logic) 47 - [Hoare triples](hoare-logic#hoare-triples) 48 - [Semantic approach to Hoare Logic](hoare-logic#semantic-approach-to-hoare-logic) 49 - [Verification condition generator](hoare-logic#verification-condition-generator) 50 - [Hoare triples for total correctness](hoare-logic#hoare-triples-for-total-correctness) 51 - [Denotational semantics](denotational-semantics) 52 - [Compositionality](denotational-semantics#compositionality) 53 - [Relational denotational semantics](denotational-semantics#relational-denotational-semantics) 54 - [Fixpoints](denotational-semantics#fixpoints) 55 - [Monotone functions](denotational-semantics#monotone-functions) 56 - [Complete lattices](denotational-semantics#complete-lattices) 57 - [Least fixpoint](denotational-semantics#least-fixpoint) 58 - [Application to program equivalence](denotational-semantics#application-to-program-equivalence) 59 - [Logical foundations of mathematics](logical-foundations-of-mathematics) 60 - [Universes](logical-foundations-of-mathematics#universes) 61 - [The Prop universe](logical-foundations-of-mathematics#the-prop-universe) 62 - [Universe of α → β (impredicativity)](logical-foundations-of-mathematics#universe-of-a-b-impredicativity) 63 - [Proof irrelevance](logical-foundations-of-mathematics#proof-irrelevance) 64 - [No large elimination](logical-foundations-of-mathematics#no-large-elimination) 65 - [Axiom of choice](logical-foundations-of-mathematics#axiom-of-choice) 66 - [Subtypes](logical-foundations-of-mathematics#subtypes) 67 - [Quotient types](logical-foundations-of-mathematics#quotient-types) 68 - [Basic mathematical structures](basic-mathematical-structures) 69 - [Type classes](basic-mathematical-structures#type-classes) 70 - [Lists, multisets, finite sets](basic-mathematical-structures#lists-multisets-finite-sets) 71 - [Order type classes](basic-mathematical-structures#order-type-classes) 72 - [Rational and real numbers](rational-and-real-numbers) 73 - [Rational numbers](rational-and-real-numbers#rational-numbers) 74 - [Real numbers](rational-and-real-numbers#real-numbers) 75 - [Formalizing the p-adic numbers](formalizing-the-p-adic-numbers) 76 - [The p-adic norm](formalizing-the-p-adic-numbers#the-p-adic-norm)