Symbols: Special symbols

Preface

• Welcome
• Overview
  • Logic
  • Proof Assistants
  • Functional Programming
  • Program Verification
  • Type Systems
• Practicalities
  • System Requirements
  • Exercises
  • Chapter Dependencies
  • Downloading the Coq Files
• Note for Instructors
• Translations

Basics: Functional Programming in Coq

• Introduction
• Enumerated Types
  • Days of the Week
  • Booleans
  • Function Types
  • Numbers
• Proof by Simplification
• Proof by Rewriting
• Proof by Case Analysis
• More Exercises
• Optional Material
  • More on Notation
  • Fixpoints and Structural Recursion

Induction: Proof by Induction

• Naming Cases
• Proof by Induction
• Proofs Within Proofs
• More Exercises
• Advanced Material
  • Formal vs. Informal Proof

Lists: Working with Structured Data

• Pairs of Numbers
• Lists of Numbers
  • Bags via Lists
• Reasoning About Lists
  • Micro-Sermon
  • Induction on Lists
  • SearchAbout
  • List Exercises, Part 1
  • List Exercises, Part 2
• Options
• Dictionaries

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
  • Map for options
  • Fold
  • Functions For Constructing Functions
• The unfold Tactic
• Additional Exercises

MoreCoq: More About Coq

• The apply Tactic
• The apply ... with ... Tactic
• The inversion tactic
• Using Tactics on Hypotheses
• Varying the Induction Hypothesis
• Using destruct on Compound Expressions
• Review
• Additional Exercises

Logic: Logic in Coq

• Propositions
• Proofs and Evidence
  • Implications are functions
  • Defining Propositions
• Conjunction (Logical "and")
  • "Introducing" Conjuctions
  • "Eliminating" conjunctions
• Iff
• Disjunction (Logical "or")
  • Implementing Disjunction
  • Relating ∧ and ∨ with andb and orb (advanced)
• Falsehood
  • Truth
• Negation
  • Inequality

Prop: Propositions and Evidence

• • From Boolean Functions to Propositions
  • Inductively Defined Propositions
• Inductively Defined Propositions
  • Inference Rules
  • Induction Over Evidence
  • Inversion on Evidence
  • inversion revisited
• Additional Exercises
• Relations
• Programming with Propositions Revisited

MoreLogic

• More Logic
• Existential Quantification
• Evidence-carrying booleans.
• Additional Exercises

ProofObjects: Working with Explicit Evidence in Coq

• • Proof Scripts and Proof Objects
  • Quantification, Implications and Functions
  • Giving Explicit Arguments to Lemmas and Hypotheses
  • Programming with Tactics (Optional)

MoreInd: More on Induction

• Induction Principles
  • Induction Hypotheses
  • More on the induction Tactic
  • Generalizing Inductions.
• Informal Proofs (Advanced)
  • Informal Proofs by Induction
• Optional Material
  • Induction Principles in Prop
• Additional Exercises
  • Induction Principles for other Logical Propositions
  • Explicit Proof Objects for Induction
  • The Coq Trusted Computing Base

Review1: Review Session for First Midterm

• General Notes
• Expressions and Their Types
• Inductive Definitions
• Tactics
• Proof Objects
• Functional Programming
• Judging Propositions
• More Type Checking

SfLib: Software Foundations Library

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

Imp: Simple Imperative Programs

• Arithmetic and Boolean Expressions
  • Syntax
  • Evaluation
  • Optimization
• Coq Automation
  • Tacticals
  • Defining New Tactic Notations
  • The omega Tactic
  • A Few More Handy Tactics
• Evaluation as a Relation
  • Inference Rule Notation
  • Equivalence of the Definitions
  • Computational vs. Relational Definitions
• Expressions With Variables
  • Identifiers
  • States
  • Syntax
  • Evaluation
• Commands
  • Syntax
  • Examples
• Evaluation
  • Evaluation as a Function (Failed Attempt)
  • Evaluation as a Relation
  • Determinism of Evaluation
• Reasoning About Imp Programs
• Additional Exercises

ImpParser: Lexing and Parsing in Coq

• Internals
  • Lexical Analysis
  • Parsing
• Examples

ImpCEvalFun: Evaluation Function for Imp

• • Evaluation Function
  • Equivalence of Relational and Step-Indexed Evaluation
  • Determinism of Evaluation (Simpler Proof)

Extraction: Extracting ML from Coq

• Basic Extraction
• Controlling Extraction of Specific Types
• A Complete Example
• Discussion

Equiv: Program Equivalence

• Behavioral Equivalence
  • Definitions
  • Examples
  • The Functional Equivalence Axiom
• Properties of Behavioral Equivalence
  • Behavioral Equivalence is an Equivalence
  • Behavioral Equivalence is a Congruence
• Program Transformations
  • The Constant-Folding Transformation
  • Soundness of Constant Folding
• Proving That Programs Are Not Equivalent
• Extended exercise: Non-deterministic Imp
• Doing Without Extensionality (Optional)
• Additional Exercises

Hoare: Hoare Logic, Part I

• Hoare Logic
  • Assertions
  • Hoare Triples
  • Proof Rules
• Hoare Logic: So Far
  • Hoare Logic Rules (so far)
  • Exercise: HAVOcC
  • Complete List of Hoare Logic Rules

Hoare2: Hoare Logic, Part II

• Decorated Programs
  • Example: Swapping Using Addition and Subtraction
  • Example: Simple Conditionals
  • Example: Reduce to Zero (Trivial Loop)
  • Example: Division
• Finding Loop Invariants
  • Example: Slow Subtraction
  • Exercise: Slow Assignment
  • Exercise: Slow Addition
  • Example: Parity
  • Example: Finding Square Roots
  • Example: Squaring
  • Exercise: Factorial
  • Exercise: Min
  • Exercise: Power Series
• Weakest Preconditions (Advanced)
• Formal Decorated Programs (Advanced)
  • Syntax
  • Extracting Verification Conditions
  • Examples

Smallstep: Small-step Operational Semantics

• A Toy Language
• Relations
  • Values
  • Strong Progress and Normal Forms
• Multi-Step Reduction
  • Examples
  • Normal Forms Again
  • Equivalence of Big-Step and Small-Step Reduction
  • Additional Exercises
• Small-Step Imp
• Concurrent Imp
• A Small-Step Stack Machine

Review2: Review Session for Second Midterm

• General Notes
• Definitions
• IMP Program Equivalence
• Hoare triples
• Decorated programs

Auto: More Automation

• The auto and eauto tactics
• Searching Hypotheses

Types: Type Systems

• Typed Arithmetic Expressions
  • Syntax
  • Operational Semantics
  • Normal Forms and Values
  • Typing
  • Canonical forms
  • Progress
  • Type Preservation
  • Type Soundness
• Aside: the normalize Tactic
  • Additional Exercises

Stlc: The Simply Typed Lambda-Calculus

• The Simply Typed Lambda-Calculus
  • Overview
  • Syntax
  • Operational Semantics
  • Typing

StlcProp: Properties of STLC

• Canonical Forms
• Progress
• Preservation
  • Free Occurrences
  • Substitution
  • Main Theorem
• Type Soundness
• Uniqueness of Types
• Additional Exercises
  • Exercise: STLC with Arithmetic

MoreStlc: More on the Simply Typed Lambda-Calculus

• Simple Extensions to STLC
  • Numbers
  • let-bindings
  • Pairs
  • Unit
  • Sums
  • Lists
  • General Recursion
  • Records
• Exercise: Formalizing the Extensions
  • Examples
  • Properties of Typing

Sub: Subtyping

• Concepts
  • A Motivating Example
  • Subtyping and Object-Oriented Languages
  • The Subsumption Rule
  • The Subtype Relation
  • Exercises
• Formal Definitions
  • Core Definitions
  • Subtyping
  • Typing
  • Typing examples
• Properties
  • Inversion Lemmas for Subtyping
  • Canonical Forms
  • Progress
  • Inversion Lemmas for Typing
  • Context Invariance
  • Substitution
  • Preservation
  • Records, via Products and Top
  • Exercises
• Exercise: Adding Products