Preface

• Overview
• Practicalities
  • Required Background
• Coq
  • System Requirements
  • Access to the Coq files
• Exercises
• Recommended Reading
• For Instructors

Basics: Functional Programming and Reasoning About Programs

• Enumerated Types
  • Days of the Week
  • Booleans
  • Function Types
  • Numbers
• 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
  • Bags via lists
• Reasoning about lists
  • Induction on lists
• Options
• The apply tactic
• Varying the Induction Hypothesis
• Additional Exercises

Poly: Polymorphism and Higher-Order Functions

• Polymorphism
  • Polymorphic Lists
  • Polymorphic Pairs
  • Polymorphic Options
• Functions as Data
  • Higher-Order Functions
  • Partial Application
  • Digression: Currying
  • Filter
  • Anonymous Functions
  • Map
  • Fold
  • Functions For Constructing Functions
• More About Coq
  • The unfold Tactic
  • Inversion
  • Using Tactics on Hypotheses
  • Using destruct on Compound Expressions
  • The remember Tactic
  • The apply ... with ... Tactic
  • Additional Exercises

Ind: Propositions and Evidence

• Review
• Programming with Propositions
• Evidence
  • Inductively Defined Propositions
  • The Curry-Howard Correspondence
  • Implication
  • Induction Principles for Inductively Defined Types
  • Induction Hypotheses
  • A Closer Look at the induction Tactic
  • Reasoning by Induction Over Evidence
  • Why Define Propositions Inductively?
  • Induction Principles in Prop
• The Big Picture: Coq's Two Universes
  • Values
  • Inductive Definitions
  • Functions and Quantifiers
  • Functions and Implications
  • Propositions and Booleans
• Generalizing Induction Hypotheses
• Templates for Informal Proofs by Induction
  • Proof by Induction Over an Inductively Defined Set
  • Induction Over an Inductively Defined Proposition
• Additional Exercises

Logic: Logic in Coq

• Quantification and Implication
• Conjunction
  • Iff
• Disjunction
  • Digression: Induction Principles for /\ and \/
  • Relating /\ and \/ with andb and orb
• Falsehood
  • Truth
• Negation
  • Inequality
• Existential Quantification
• Equality
  • Inversion, Again
• Relations as Propositions
  • Digression: More Facts about <= and <
• Informal Proofs, Again
• Explicit Proof Objects for Induction.
• The Coq Trusted Computing Base.

Rel: Properties of Relations

• Relations
• Properties
• Reflexive, Transitive Closure

SfLib: Software Foundations Library

• From the Coq Standard Library
• From Basics.v
• From Props.v
• From Logic.v
• Some useful tactics

Imp: Simple Imperative Programs

• Arithmetic and Boolean Expressions
  • Syntax
  • Evaluation
  • Optimization
• Coq Automation
  • Tacticals
  • Defining New Tactic Notations
  • Relational Presentation of Evaluation
  • Inference Rule Notation
  • The omega Tactic
  • A Few More Handy Tactics
• Expressions With Variables
  • Identifiers
  • States
  • Syntax
  • Evaluation
• Commands
  • Syntax
  • Examples
• Evaluation
  • Evaluation Function
  • Evaluation Relation
  • Equivalence of Relational and Step-Indexed Evaluation
  • Determinacy of Evaluation
• Reasoning About Programs
• Additional Exercises

ImpParser: Lexing and Parsing in Coq

• Internals
  • Lexical Analysis
  • Parsing
• Examples

Equiv: Program Equivalence

• Behavioral Equivalence
  • Definitions
  • Examples
  • A Digression on Equivalences.
  • Program Equivalence is an Equivalence
  • Program Equivalence is a Congruence
• Case Study: Constant Folding
  • Soundness of Program Transformations
  • The Constant-Folding Transformation
  • Soundness of Constant Folding
  • Soundness of (0 + n) Elimination
• Proving That Programs Are Not Equivalent
• Reasoning about Imp programs
• Additional Exercises

Hoare: Hoare Logic

• Hoare Logic
  • Assertions
  • Hoare Triples
  • Weakest Preconditions
  • Proof Rules
  • Decorated Programs
• Using Hoare Logic to Reason About Programs
  • Miscellaneous Lemmas
  • Example: Slow Subtraction
  • Exercise: Reduce to Zero
  • Exercise: Slow Addition
  • Example: Parity
  • Example: Finding Square Roots
  • Exercise: Factorial

MoreHoare: Hoare Logic with Lists; Formalizing Decorated Programs

• Hoare Logic with Lists
  • Extensions
  • Repeated Definitions
  • Examples
• Hoare Logic as a Logic
• Formalizing Decorated Programs
  • Syntax
  • Extracting Verification Conditions
  • Examples

Smallstep: Small-step Operational Semantics

• A Toy Language
  • Values
  • Normal Forms
  • Exercises
• Multi-Step Reduction
  • Multi-Step Reduction
  • Normal Forms Again
  • Equivalence of Big-Step and Small-Step Reduction
  • Additional Exercises
• Small-Step Imp
• Concurrent Imp

Stlc: The Simply Typed Lambda-Calculus

• More Automation
  • The auto and eauto Tactics
  • The Proof with Tactic
  • The solve by inversion Tactic
  • The try solve Tactic
  • The f_equal Tactic
  • The normalize Tactic
• Typed Arithmetic Expressions
  • Syntax
  • Small-Step Reduction
  • Normal Forms and Values
  • Typing
  • Progress
  • Type Preservation
  • Type Soundness
  • Additional Exercises
• The Simply Typed Lambda-Calculus
  • Syntax and Operational Semantics
  • Typing
  • Properties
  • Additional Exercises
• Exercise: STLC with Arithmetic
  • Syntax and Operational Semantics

MoreStlc: More on the Simply Typed Lambda-Calculus

• Typechecking for STLC
  • Comparing Types
  • The Typechecker
  • Properties
• Simple Extensions to STLC
• Formalizing the Extensions
  • Examples
  • Properties of Typing

Records: Adding Records to STLC

• Adding Records
• Formalizing Records
  • Examples
  • Properties of Typing

References: Typing Mutable References

• Mutable References
  • Syntax
  • Pragmatics
  • Operational Semantics
  • Typing
  • Safety
• References and Nontermination
• Additional Exercises

Subtyping: Subtyping

• Concepts
  • A Motivating Example
  • Subtyping and Object-Oriented Languages
  • The Subsumption Rule
  • The Subtype Relation
• Core definitions
  • Definition
  • Subtyping Examples and Exercises
• Typing
  • Typing examples
• Properties
  • Inversion Lemmas for Subtyping
  • Progress
  • Inversion Lemmas for Typing
  • Context Invariance
  • Substitution
  • Preservation
  • Exercises on Typing

RecordSub: Subtyping with Records

• Core Definitions
• Subtyping
  • Definition
  • Subtyping Examples and Exercises
  • Properties of Subtyping
• Typing
  • Typing Examples
  • Properties of Typing
  • Exercises on Typing

Norm: Normalization of STLC

• Language
• Normalization
  • Membership in R_T is invariant under evaluation
  • Closed instances of terms of type T belong to R_T