# 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.

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

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

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