---
title: "Introduction to Higher Order Categorical Logic"
authors:
  - "Joachim Lambek"
  - "Philip J. Scott"
year: 1986
venue: "Cambridge University Press"
arxiv: null
doi: "10.1017/CBO9780511620263"
source: "https://doi.org/10.1017/CBO9780511620263"
topics:
  - category-theory
  - lambda-calculus
  - cartesian-closed
  - logic
seed_rank: 41
seed_batch: "prefill-2026-08-13"
reviewed: "2026-08-13"
pool: "maths-foundations"
relevance_score: 10
cites:
  - title: "From λ-calculus to Cartesian Closed Categories"
    url: "https://math.ucr.edu/home/baez/qg-fall2006/ccc.html"
    year: 1980
    arxiv: null
    doi: null
  - title: "Cartesian Closed Categories and Typed λ-Calculi"
    url: "https://doi.org/10.1007/3-540-17184-3_44"
    year: 1986
    arxiv: null
    doi: "10.1007/3-540-17184-3_44"
  - title: "Physics, Topology, Logic and Computation: A Rosetta Stone"
    url: "https://arxiv.org/abs/0903.0340"
    year: 2011
    arxiv: "0903.0340"
    doi: "10.1007/978-3-642-12821-9_2"
see:
  - "044-from-calculus-to-cartesian-closed-categories"
  - "151-cartesian-closed-categories-and-typed-calculi"
  - "018-physics-topology-logic-and-computation-a-rosetta-stone"
---

# Introduction to Higher Order Categorical Logic

## One-sentence takeaway

Lambek and Scott prove the equivalence of typed λ-calculi, cartesian closed categories, and a form of higher-order intuitionistic logic — the book that made “types are objects, terms are morphisms” a theorem.

## Why it matters here

Every “compile to categories” or “ano is the internal language of a CCC with effects” claim bottoms out here. This is the bible; the 1980 Curry-festschrift essay is the teaser.

## Key ideas

- Part I develops cartesian closed categories and the interpretation of simply-typed λ-calculus: products are pairing, exponentials are function types, evaluation is application.
- The internal language of a CCC is a typed λ-calculus; conversely every typed λ-theory presents a CCC. That correspondence is an equivalence of categories, not a slogan.
- Part II lifts the story to toposes and higher-order logic, so quantification and power objects enter once you leave the simply-typed fragment.
- Written as a graduate text (Cambridge Studies in Advanced Mathematics 7); assumes Mac Lane-level comfort with adjunctions.
- CUP DOI 10.1017/CBO9780511620263; paperback reprint 1988 is the copy most libraries hold.

## Caveats

## Links

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