Cambridge University Press, 2016.

My purpose in writing this book is to establish a comprehensive framework for formulating and analyzing a broad range of ideas in programming languages. If language design and programming methodology are to advance from a trade-craft to a rigorous discipline, it is essential that we first get the definitions right. Then, and only then, can there be meaningful analysis and consolidation of ideas. My hope is that I have helped to build such a foundation.

Abbreviated online edition, with corrections.

- Sample solutions to the printed exercises. (Password: "pfpl-solutions")
- More exercises, with answers.

- The Structure of an Interpreter.
- Church's λ-Calculus.
- Dynamic Dispatch as an Abstract Type.
- Natural and Co-Natural Numbers.
- Equality of T and F.
- Recursive, Inductive, and Coinductive Types.
- PCF By Value.
- Stacks By-Name and By-Value.
- Programming with Continuations.
- CPS Transformation.
- Types and Parallelism.
- Relating Transition and Cost Dynamics for Parallel PCF.
- Exceptions: Control and Data.
- Automata and Concurrency.
- Modernized Concurrent Algol.
- Derived Forms for Modernized Algol.
- Types for Program Modules.
- Tarski's Theorem.
- How to (Re)Invent Tait's Method.
- How to (Re)Invent Girard's Method.
- Reynolds's Parametricity Theorem, Directly.

- Principles of Programming Languages. Carnegie Mellon University undergraduate course in programming languages.
- Existential Type Blog. Writings on programming languages, research, and education.
- Notation Guide provided by Toronto CS Reading Group.

Last modified: Mon Apr 25 21:02:30 EDT 2016