Software Foundations

The interactive textbook Software Foundations, by Benjamin C. Pierce et al., introduces logic, the Coq proof assistant, and applications to the theory of programming languages. It has been used at universities around the world (and for independent study) since 2008.

For DeepSpec, the textbook has been rewritten and expanded. In Spring 2017 we will be dividing the material on logic and programming languages into two volumes, 1. Logical Foundations and 2. Programming Language Foundations. A new volume, 3. Verified Functional Algorithms by Andrew W. Appel, is for those who want to teach (or learn) the verification of programs and not only programming languages. Volume 3 depends on material only from Volume 1. An instructor can teach Volume 1 in half a semester, then choose material from Volumes 2 and 3 for the second half of the semester.

Volume 4. Separation Logic by Arthur Charguéraud is in preparation. Volume 5. Systems Verification is planned for the future.

Logical Foundations
by Benjamin C. Pierce et al.

Contents

  • Preface
  • Basics: Functional Programming in Coq
  • Induction: Proof by Induction
  • Lists: Working with Structured Data
  • Poly: Polymorphism and Higher-Order Functions
  • Tactics: More Basic Tactics
  • Logic: Logic in Coq
  • IndProp: Inductively Defined Propositions
  • Maps: Total and Partial Maps
  • ProofObjects: The Curry-Howard Correspondence
  • IndPrinciples: Induction Principles
  • Rel: Properties of Relations
Programming Language Foundations
by Benjamin C. Pierce et al.

Contents

  • Imp: Simple Imperative Programs
  • ImpParser: Lexing and Parsing in Coq
  • ImpCEvalFun: Evaluation Function for Imp
  • Extraction: Extracting ML from Coq
  • Equiv: Program Equivalence
  • Hoare: Hoare Logic, Part I
  • Hoare2: Hoare Logic, Part II
  • HoareAsLogic: Hoare Logic as a Logic
  • Smallstep: Small-step Operational Semantics
  • Auto: More Automation
  • Types: Type Systems
  • Stlc: The Simply Typed Lambda-Calculus
  • StlcProp: Properties of STLC
  • MoreStlc: More on the Simply Typed Lambda-Calculus
  • Sub: Subtyping
  • Typechecking: A Typechecker for STLC
  • Records: Adding Records to STLC
  • References: Typing Mutable References
  • RecordSub: Subtyping with Records
  • Norm: Normalization of STLC
  • LibTactics: A Collection of Handy General-Purpose Tactics
  • UseTactics: Tactic Library for Coq: A Gentle Introduction
  • UseAuto: Theory and Practice of Automation in Coq Proofs
  • PE: Partial Evaluation
  • Postscript
Verified Functional Algorithms
by Andrew W. Appel

Contents

  • VFA: Verified Functional Algorithms
  • Perm: Basic techniques for permutations and ordering
  • Sort: Insertion sort
  • Multiset: Insertion sort with multisets
  • Selection: Selection sort, with specification and proof of correctness
  • SearchTree: Binary search trees
  • ADT: Abstract data types
  • Extraction: Running Coq programs in ML
  • Redblack: Implementation and proof of red-black trees
  • Trie: Number representations and efficient lookup tables
  • Priqueue: Priority queues
  • Binom: Binomial queues
  • Decide: programming with decision procedures
  • Color: Graph coloring