Volume 2: Programming Language Foundations

  • Table of Contents
    •
  • Index
    •
  • Roadmap
    •

Preface

  • Top
  • Welcome
  • Overview
    • Program Verification
    • Type Systems
    • Further Reading
  • Note for Instructors
  • Thanks

Program Equivalence    (Equiv)

  • Top
  • Behavioral Equivalence
    • Definitions
    • Simple Examples
  • 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 Inequivalence
  • Extended Exercise: Nondeterministic Imp
  • Additional Exercises

Hoare Logic, Part I    (Hoare)

  • Top
  • Assertions
  • Hoare Triples
  • Proof Rules
    • Assignment
    • Consequence
    • Digression: The eapply Tactic
    • Skip
    • Sequencing
    • Conditionals
    • Loops
  • Summary
  • Additional Exercises

Hoare Logic, Part II    (Hoare2)

  • Top
  • Decorated Programs
    • Example: Swapping Using Addition and Subtraction
    • Example: Simple Conditionals
    • Example: Reduce to Zero
    • 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
  • Formal Decorated Programs
    • Syntax
    • Extracting Verification Conditions
    • Automation
    • Examples
    • Further Exercises

Hoare Logic as a Logic    (HoareAsLogic)

  • Top
  • Definitions
  • Properties

Small-step Operational Semantics    (Smallstep)

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

Type Systems    (Types)

  • Top
  • Typed Arithmetic Expressions
    • Syntax
    • Operational Semantics
    • Normal Forms and Values
    • Typing
    • Progress
    • Type Preservation
    • Type Soundness
    • Additional Exercises

The Simply Typed Lambda-Calculus    (Stlc)

  • Top
  • Overview
  • Syntax
    • Types
    • Terms
  • Operational Semantics
    • Values
    • Substitution
    • Reduction
    • Examples
  • Typing
    • Contexts
    • Typing Relation
    • Examples

Properties of STLC    (StlcProp)

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

More on the Simply Typed Lambda-Calculus    (MoreStlc)

  • Top
  • Simple Extensions to STLC
    • Numbers
    • Let Bindings
    • Pairs
    • Unit
    • Sums
    • Lists
    • General Recursion
    • Records
  • Exercise: Formalizing the Extensions
    • Examples
    • Properties of Typing

Subtyping    (Sub)

  • Top
  • Concepts
    • A Motivating Example
    • Subtyping and Object-Oriented Languages
    • The Subsumption Rule
    • The Subtype Relation
    • Exercises
  • Formal Definitions
    • Core Definitions
    • Subtyping
    • Typing
  • Properties
    • Inversion Lemmas for Subtyping
    • Canonical Forms
    • Progress
    • Inversion Lemmas for Typing
    • Context Invariance
    • Substitution

A Typechecker for STLC    (Typechecking)

  • Top
  • Comparing Types
  • The Typechecker
  • Digression: Improving the Notation
  • Properties
  • Exercises

Adding Records to STLC    (Records)

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

Typing Mutable References    (References)

  • Top
  • Definitions
  • Syntax
  • Pragmatics
    • Side Effects and Sequencing
    • References and Aliasing
    • Shared State
    • Objects
    • References to Compound Types
    • Null References
    • Garbage Collection
  • Operational Semantics
    • Locations
    • Stores
    • Reduction
  • Typing
    • Store typings
    • The Typing Relation
  • Properties
    • Well-Typed Stores
    • Extending Store Typings
    • Preservation, Finally
    • Substitution Lemma
    • Assignment Preserves Store Typing
    • Weakening for Stores
    • Preservation!
    • Progress
  • References and Nontermination
  • Additional Exercises

Subtyping with Records    (RecordSub)

  • Top
  • Core Definitions
  • Subtyping
    • Definition
    • Examples
    • Properties of Subtyping
  • Typing
    • Typing Examples
    • Properties of Typing

Normalization of STLC    (Norm)

  • Top
  • Language
  • Normalization
    • Membership in R_T Is Invariant Under Reduction
    • Closed Instances of Terms of Type t Belong to R_T

A Collection of Handy General-Purpose Tactics    (LibTactics)

  • Top
  • Tools for Programming with Ltac
    • Identity Continuation
    • Untyped Arguments for Tactics
    • Optional Arguments for Tactics
    • Wildcard Arguments for Tactics
    • Position Markers
    • List of Arguments for Tactics
    • Databases of Lemmas
    • On-the-Fly Removal of Hypotheses
    • Numbers as Arguments
    • Testing Tactics
    • Testing evars and non-evars
    • Check No Evar in Goal
    • Helper Function for Introducing Evars
    • Tagging of Hypotheses
    • More Tagging of Hypotheses
    • Deconstructing Terms
    • Action at Occurence and Action Not at Occurence
    • An Alias for eq
  • Common Tactics for Simplifying Goals Like intuition
  • Backward and Forward Chaining
    • Application
    • Assertions
    • Instantiation and Forward-Chaining
    • Experimental Tactics for Application
    • Adding Assumptions
    • Application of Tautologies
    • Application Modulo Equalities
    • Absurd Goals
  • Introduction and Generalization
    • Introduction
    • Introduction using ⇒ and =>>
    • Generalization
    • Naming
  • Rewriting
    • Replace
    • Change
    • Renaming
    • Unfolding
    • Simplification
    • Reduction
    • Substitution
    • Tactics to Work with Proof Irrelevance
    • Proving Equalities
  • Inversion
    • Basic Inversion
    • Inversion with Substitution
    • Injection with Substitution
    • Inversion and Injection with Substitution —rough implementation
    • Case Analysis
  • Induction
  • Coinduction
  • Decidable Equality
  • Equivalence
  • N-ary Conjunctions and Disjunctions
  • Tactics to Prove Typeclass Instances
  • Tactics to Invoke Automation
    • Definitions for Parsing Compatibility
    • hint to Add Hints Local to a Lemma
    • jauto, a New Automation Tactic
    • Definitions of Automation Tactics
    • Parsing for Light Automation
    • Parsing for Strong Automation
  • Tactics to Sort Out the Proof Context
    • Hiding Hypotheses
    • Sorting Hypotheses
    • Clearing Hypotheses
  • Tactics for Development Purposes
    • Skipping Subgoals
  • Compatibility with standard library

Tactic Library for Coq: A Gentle Introduction    (UseTactics)

  • Top
  • Tactics for Naming and Performing Inversion
    • The Tactic introv
    • The Tactic inverts
  • Tactics for N-ary Connectives
    • The Tactic splits
    • The Tactic branch
  • Tactics for Working with Equality
    • The Tactics asserts_rewrite and cuts_rewrite
    • The Tactic substs
    • The Tactic fequals
    • The Tactic applys_eq
  • Some Convenient Shorthands
    • The Tactic unfolds
    • The Tactics false and tryfalse
    • The Tactic gen
    • The Tactics admits, admit_rewrite and admit_goal
    • The Tactic sort
  • Tactics for Advanced Lemma Instantiation
    • Working of lets
    • Working of applys, forwards and specializes
    • Example of Instantiations
  • Summary

Theory and Practice of Automation in Coq Proofs    (UseAuto)

  • Top
  • Basic Features of Proof Search
    • Strength of Proof Search
    • Basics
    • Conjunctions
    • Disjunctions
    • Existentials
    • Negation
    • Equalities
  • How Proof Search Works
    • Search Depth
    • Backtracking
    • Adding Hints
    • Integration of Automation in Tactics
  • Example Proofs using Automation
    • Determinism
    • Preservation for STLC
    • Progress for STLC
    • BigStep and SmallStep
    • Preservation for STLCRef
    • Progress for STLCRef
    • Subtyping
  • Advanced Topics in Proof Search
    • Stating Lemmas in the Right Way
    • Unfolding of Definitions During Proof-Search
    • Automation for Proving Absurd Goals
    • Automation for Transitivity Lemmas
  • Decision Procedures
    • Omega
    • Ring
    • Congruence
  • Summary

Partial Evaluation    (PE)

  • Top
  • Generalizing Constant Folding
    • Partial States
    • Arithmetic Expressions
    • Boolean Expressions
  • Partial Evaluation of Commands, Without Loops
    • Assignment
    • Conditional
    • The Partial Evaluation Relation
    • Examples
    • Correctness of Partial Evaluation
  • Partial Evaluation of Loops
    • Examples
    • Correctness
  • Partial Evaluation of Flowchart Programs
    • Basic blocks
    • Flowchart programs
    • Partial Evaluation of Basic Blocks and Flowchart Programs

Postscript

  • Top
  • Looking Back
  • Looking Around
  • Looking Forward

Bibliography    (Bib)

  • Top
  • Resources cited in this volume