Preface
Basics: Functional programming and reasoning about programs
- Coq
- Enumerated Types
- Proof By Simplification
- The intros tactic
- Proof by rewriting
- Case analysis
- Naming cases
- Induction
- Formal vs. informal proof
- Proofs Within Proofs
- Extra Exercises
Lists: Products, Lists and Options
- Pairs of numbers
- Lists of numbers
- Reasoning about lists
- Options
- The apply tactic
- Varying the Induction Hypothesis
- Additional Exercises
Poly: Polymorphism and Higher-Order Functions
Props: Programming with Propositions
Logic: Logic in Coq
- Conjunction
- Iff
- Disjunction
- Relating /\ and \/ with andb and orb
- Falsehood
- Truth
- Negation
- Inequality
- Existential quantification
- Equality.
- Inversion, again
- Relations as propositions
- Relations, in General
- More facts about <= and <
SfLib: Software Foundations Library
Imp: Simple imperative programs
- Templates for informal proofs by induction
- Evaluating arithmetic expressions
- Correctness of a simple optimization
- Tacticals
- Defining new tactic notations
- While programs
- Evaluation
- Equivalence of step-indexed and relational evaluation
- Reasoning about programs
Equiv: Program equivalence
- One more tactic
- Notation for evaluation
- Determinacy of evaluation
- Behavioral equivalence
- Case study: Constant folding
- Soundness of constant folding
- Soundness of (0 + n) elimination
- Case study: Proving that programs are NOT equivalent
- Reasoning about Imp programs
- Additional exercises
Hoare: Hoare Logic
- Assertions
- Hoare triples
- Weakest preconditions
- Proof rule for assignment
- Rules of consequence
- The eapply tactic
- Proof rule for SKIP
- Proof rule for ;
- Proof rule for conditionals
- Proof rule for loops
- Decorated programs
- Using Hoare Logic to reason about programs
Smallstep: Small-step operational semantics
Stlc: The Simply Typed Lambda-Calculus
- More Automation
- Typed arithmetic expressions
- The Simply Typed Lambda-Calculus
- Properties
- STLC with arithmetic
MoreStlc: More on the Simply Typed Lambda-Calculus
Subtyping: Subtyping
This page has been generated by coqdoc