---
title: "Functionality in Combinatory Logic"
authors:
  - "Haskell B. Curry"
year: 1934
venue: "Proceedings of the National Academy of Sciences"
arxiv: null
doi: "10.1073/pnas.20.11.584"
source: "https://doi.org/10.1073/pnas.20.11.584"
topics:
  - curry-howard
  - types
  - combinatory-logic
seed_rank: 498
seed_batch: "foundations-greats-2026-08-13"
reviewed: "2026-08-13"
pool: "maths-foundations"
relevance_score: 9
lineage: foundations-of-computing
cites:
  - title: "Grundlagen der kombinatorischen Logik"
    url: "https://doi.org/10.2307/2370619"
    year: 1930
    doi: "10.2307/2370619"
see:
  - "497-grundlagen-der-kombinatorischen-logik"
---

# Functionality in Combinatory Logic

## One-sentence takeaway

Curry assigns combinators *functional characters* — type-like classifications such as \(F\alpha\beta\) for “function from \(\alpha\) to \(\beta\)” — so a term's construction is also a derivation that it has that character.

## Why it matters here

Prehistory of Curry–Howard: the same paper lineage that later meets typed λ and the effect/type systems already in the corpus.

## Key ideas

- Functionality is a primitive illative notion, not a set-theoretic graph: \(F\) classifies combinators by how they transform other combinators.
- A well-formed combination that has a functional character is already a typed term; ill-typed combinations are simply not theorems.
- Direct ancestor of Hindley's principal-type algorithm for combinatory logic (1969) and of the propositions-as-types slogan.
- Short PNAS note (20:584–590, 1934) condensing the typed fragment of the 1930 foundation.

## Caveats

## Links

- DOI: [10.1073/pnas.20.11.584](https://doi.org/10.1073/pnas.20.11.584)