Volume 2: Programming Language Foundations
Table of Contents
Index
Roadmap
Preface
Welcome
Overview
Program Verification
Type Systems
Further Reading
Practicalities
Recommended Citation Format
Note for Instructors
Thanks
Program Equivalence (
Equiv
)
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
Proving Inequivalence
Hoare Logic, Part I (
Hoare
)
Assertions
Notations for Assertions
Hoare Triples, Informally
Hoare Triples, Formally
Proof Rules
Skip
Sequencing
Assignment
Consequence
Automation
Sequencing + Assignment
Conditionals
While Loops
Summary
Additional Exercises
Havoc
Assert and Assume
Hoare Logic, Part II (
Hoare2
)
Decorated Programs
Example: Swapping
Example: Simple Conditionals
Example: Reduce to Zero
Example: Division
From Decorated Programs to Formal Proofs
Formal Decorated Programs
Syntax
Extracting Verification Conditions
Automation
Finding Loop Invariants
Example: Slow Subtraction
Exercise: Slow Assignment
Exercise: Minimum
Exercise: Two Loops
Hoare Logic as a Logic (
HoareAsLogic
)
Hoare Logic and Model Theory
Hoare Logic and Proof Theory
Derivability
Soundness and Completeness
Postscript: Decidability
Small-step Operational Semantics (
Smallstep
)
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
)
Typed Arithmetic Expressions
Syntax
Operational Semantics
Normal Forms and Values
Typing
Progress
Type Preservation
Type Soundness
Additional Exercises
The Simply Typed Lambda-Calculus (
Stlc
)
Overview
Syntax
Types
Terms
Operational Semantics
Values
Substitution
Reduction
Examples
Typing
Contexts
Typing Relation
Examples
Properties of STLC (
StlcProp
)
Canonical Forms
Progress
Preservation
The Weakening Lemma
The Substitution Lemma
Main Theorem
Type Soundness
Uniqueness of Types
Context Invariance (Optional)
Exercise: STLC with Arithmetic
The Technical Theorems
Postscript
Looking Back
Looking Around
Looking Forward
Bibliography (
Bib
)
Resources cited in this volume
