---
title: "The Lambda Calculus: Its Syntax and Semantics"
authors:
  - "Henk P. Barendregt"
year: 1984
venue: "North-Holland (Studies in Logic)"
arxiv: null
doi: "10.1016/C2009-0-14309-X"
source: "https://doi.org/10.1016/C2009-0-14309-X"
topics:
  - lambda-calculus
  - barendregt
  - textbook
  - syntax-semantics
seed_rank: 708
seed_batch: "perfects-pl-2026-08-13"
reviewed: "2026-08-13"
pool: "languages"
relevance_score: 10
lineage: programming-language-foundations
cites:
  - title: "Call-by-Name, Call-by-Value and the λ-Calculus"
    url: "https://doi.org/10.1016/0304-3975(75)90017-1"
    year: 1975
    arxiv: null
    doi: "10.1016/0304-3975(75)90017-1"
  - title: "The Mechanical Evaluation of Expressions"
    url: "https://doi.org/10.1093/comjnl/6.4.308"
    year: 1964
    arxiv: null
    doi: "10.1093/comjnl/6.4.308"
see:
  - "627-call-by-name-call-by-value-and-the-lambda-calculus"
  - "617-the-mechanical-evaluation-of-expressions"
---

# The Lambda Calculus: Its Syntax and Semantics

## One-sentence takeaway

The untyped λ-calculus is developed as a mathematical object: conversion, reduction strategies, solvability, Böhm trees, and models, not as a programming-language tutorial.

## Why it matters here

Every Anoptic discussion of closures, substitution, or “what does this combinator mean” bottoms out in this book. Cite Barendregt for the theorems; cite TAPL/PFPL for the typed programming-language reading.

## Key ideas

- Syntax, α-conversion, β-reduction, and the Church–Rosser theorem are treated as the core equational theory.
- Solvability, Böhm trees, and the theory of sensible λ-theories classify which terms behave like programs.
- Models (term models, D∞, Pω) show that the equational theory has a denotational reading.
- Reduction strategies and standardization sit beside Plotkin’s CBN/CBV distinction rather than replacing it.
- The 1984 revised North-Holland volume (Studies in Logic 103) is the standard reference edition.

## Caveats

## Links

- DOI: [10.1016/C2009-0-14309-X](https://doi.org/10.1016/C2009-0-14309-X)
- ScienceDirect volume: https://www.sciencedirect.com/bookseries/studies-in-logic-and-the-foundations-of-mathematics/vol/103/suppl/C