---
title: "Practical Foundations for Programming Languages"
authors:
  - "Robert Harper"
year: 2016
venue: "Cambridge University Press (2nd ed.)"
arxiv: null
doi: "10.1017/CBO9781316576892"
source: "https://doi.org/10.1017/CBO9781316576892"
topics:
  - pfpl
  - harper
  - type-systems
  - semantics
  - textbook
seed_rank: 646
seed_batch: "perfects-pl-2026-08-13"
reviewed: "2026-08-13"
pool: "languages"
relevance_score: 10
lineage: programming-language-foundations
cites:
  - title: "Types and Programming Languages"
    url: "https://www.cis.upenn.edu/~bcpierce/tapl/"
    year: 2002
    arxiv: null
    doi: null
  - title: "The Definition of Standard ML (Revised)"
    url: "https://mitpress.mit.edu/9780262631815/the-definition-of-standard-ml/"
    year: 1997
    arxiv: null
    doi: null
  - title: "A Framework for Defining Logics"
    url: "https://doi.org/10.1145/138027.138040"
    year: 1993
    arxiv: null
    doi: "10.1145/138027.138040"
  - title: "A Structural Approach to Operational Semantics"
    url: "https://doi.org/10.1016/j.jlap.2004.05.001"
    year: 1981
    arxiv: null
    doi: "10.1016/j.jlap.2004.05.001"
see:
  - "026-types-and-programming-languages"
  - "137-the-definition-of-standard-ml-revised"
  - "651-a-framework-for-defining-logics"
  - "658-a-structural-approach-to-operational-semantics"
---

# Practical Foundations for Programming Languages

## One-sentence takeaway

Harper presents language design as twin judgments — statics (typing) and dynamics (evaluation) — with type safety as progress plus preservation.

## Why it matters here

The other canonical textbook beside TAPL, stronger on hypothetical judgments, dynamics, and modern PFPL-style presentation. The book one would steal a judgment style from when writing ano’s statics/dynamics.

## Key ideas

- Statics and dynamics as formally twin inductive definitions, not a type system plus an afterthought interpreter.
- Progress and preservation are the type-safety contract for each language fragment.
- Tour of FE, FPC, Modernized Algol, laziness, parallelism, and more, each with the same judgment discipline.
- 2nd ed. CUP 2016, DOI 10.1017/CBO9781316576892; companion to Harper–Honsell–Plotkin LF and the SML Definition.

## Caveats

## Links

- DOI: [10.1017/CBO9781316576892](https://doi.org/10.1017/CBO9781316576892)