---
title: "Advanced Topics in Types and Programming Languages"
authors:
  - "Benjamin C. Pierce (ed.)"
year: 2005
venue: "MIT Press"
arxiv: null
doi: null
source: "https://mitpress.mit.edu/9780262552677/advanced-topics-in-types-and-programming-languages/"
topics:
  - types
  - pierce
  - advanced-types
  - textbook
seed_rank: 715
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 Calculus of Constructions"
    url: "https://doi.org/10.1016/0890-5401(88)90005-3"
    year: 1988
    arxiv: null
    doi: "10.1016/0890-5401(88)90005-3"
  - title: "Linear Types Can Change the World!"
    url: "https://homepages.inf.ed.ac.uk/wadler/topics/linear-logic.html"
    year: 1990
    arxiv: null
    doi: null
see:
  - "026-types-and-programming-languages"
  - "650-the-calculus-of-constructions"
  - "148-linear-types-can-change-the-world"
---

# Advanced Topics in Types and Programming Languages

## One-sentence takeaway

ATTAPL is a sequel to TAPL: expert chapters on substructural types, dependent types, effects and regions, TAL/PCC, logical relations, and ML modules, not a second introductory textbook.

## Why it matters here

When Broadside needs a typed assembly story, a region/effect reading of engine memory, or an ML-module account of subsystems, open the relevant ATTAPL chapter instead of minting a new card for every advanced type-system paper.

## Key ideas

- Ten invited chapters: substructural types, dependent types, effect types and regions, typed assembly language, proof-carrying code, logical relations, typed operational reasoning, ML modules, type definitions, ML type inference.
- Assumes TAPL-level operational semantics and type-system technique; it is a curriculum, not a monograph with one thesis.
- Substructural and effect chapters are the ones that speak to Anoptic’s linear/region instincts; TAL/PCC speak to verified backends.
- Coquand–Huet CoC and Wadler’s linear types are representative cited ancestors of the advanced chapters.
- MIT Press hardcover 2004/2005 (ISBN 978-0-262-16228-9); later paperback 978-0-262-55267-7.

## Caveats

## Links

- MIT Press: https://mitpress.mit.edu/9780262552677/advanced-topics-in-types-and-programming-languages/
- Author page: https://www.cis.upenn.edu/~bcpierce/attapl/