Proof Terms: Reading a Derivation as a Program

Write a derivation in natural deduction and then erase the formulas, keeping only the rule names and the shape of the tree. What remains is a term. Keep the formulas and erase the rule names, and the same tree is a typing derivation. The two readings are not an analogy; they are the same tree viewed at two levels, and the correspondence is exact enough that a proof checker and a type checker can be the same program.

The dictionary

The correspondence pairs each logical rule with a typing rule for the simply typed lambda calculus.

Logic	Computation
Proposition A	Type A
Assumption A	Variable x : A
Implication A → B	Function type A → B
Proof of A	Term of type A
Assumption discharge	Lambda abstraction
Modus ponens	Application
Conjunction A ∧ B	Product type A × B
Disjunction A ∨ B	Sum type A + B
Truth ⊤	Unit type
Falsity ⊥	Empty type
Normalisation	Evaluation to a value

Each row is a rule correspondence, not merely a name correspondence. The introduction rule for implication, which discharges an assumption, becomes the typing rule for abstraction: if t : B under the assumption x : A, then λx. t : A → B. The elimination rule becomes application: from f : A → B and a : A, conclude f a : B. The side condition that the discharged assumption is not open elsewhere becomes the side condition that the bound variable does not occur free in the context.

The reading is often attributed to Curry, who observed that the types of combinators correspond to axiom schemata of implicational logic, and to Howard, who extended it to full predicate logic with quantifiers. The lambda calculus predates the observation, which is why the correspondence is a discovery about two independently developed formalisms rather than a definition.

Why normalisation is evaluation

A proof with a detour, where an introduction is immediately followed by the matching elimination, corresponds to a term with a redex. Removing the detour, as described in Natural Deduction: Why Implication Is Defined by Two Rules, substitutes a proof for an assumption. On terms, the same operation substitutes an argument for a variable.

(λx. t) u   →   t[u/x]

That is beta reduction. Proof normalisation and lambda-calculus evaluation are the same rewriting system, and the theorems transfer. Strong normalisation of the typed calculus is the statement that every reduction sequence terminates, which corresponds to the fact that every derivation normalises. Confluence is the statement that the normal form is unique, which corresponds to the fact that a derivation’s normal form does not depend on the order in which detours are removed. Subject reduction, that a term’s type is preserved by reduction, is the proof-theoretic statement that detour removal produces a derivation of the same conclusion.

The transfer is not decorative. It explains why simply typed lambda calculus is strongly normalising while the untyped calculus is not. In the typed system, every reduction decreases a measure derived from the type: the size of the type at which the redex occurs falls, and terms of a given type can only be substituted for variables of a smaller type. In the untyped system no such measure exists, and the argument to the identity function can be a term that refers to the very application being reduced, as in ω = λx. x x applied to itself, which reduces to itself in one step.

What the term structure records

A proof term is not just a certificate that a proposition holds. Its structure records how the proof was built, and different structures mean different computational content.

Consider two proofs of A → A → A. One is λx. λy. x, which discards its second argument and returns the first. The other is λx. λy. y, which does the reverse. Both prove the same proposition, and no truth-table semantics distinguishes them. The terms differ, and the difference is observable: applying each to two distinct arguments yields different results. Under the correspondence, the distinction between proofs is exactly the distinction between programs of the same type, and the question of when two proofs are the same becomes the question of when two programs are the same.

This is why proof terms matter for extraction. Given a proof of a statement with computational content, such as a formula asserting that every natural number has a factorisation, the term extracted from the derivation is a function computing the factorisation. Erasing the parts of the term that correspond to purely logical steps leaves a program; the standard technique is to mark propositions whose proofs are irrelevant and drop them during extraction. The correctness of the extracted program follows from the fact that its type is the statement, not from testing.

Connectives as data types

The correspondence extends past implication, and each extension is a claim about which programming constructs are logical.

Conjunction is a product. A proof of A ∧ B consists of a proof of A and a proof of B; a term of type A × B is a pair. The eliminations are the two projections. The local reductions, projecting from a pair that was just constructed, are the computation rules fst (a, b) = a and snd (a, b) = b.

Disjunction is a sum. A proof of A ∨ B is either a proof of A or a proof of B, tagged; a term of type A + B is a tagged value. Elimination is case analysis, and the reduction rule fires when a case split meets a tag that was just applied. The disjunction property, that a proof of A ∨ B yields a proof of one side, is the statement that a closed value of a sum type has a canonical tag, which is why an evaluator can branch on it without inspecting unevaluated code.

Truth is the unit type, with one value and no eliminations of interest. Falsity is the empty type, with no values and an elimination that is vacuous: from a value of the empty type, any type follows. That elimination is the programming analogue of ⊥-elimination, and in a total language it is a function that can never be called.

Absurdity elimination is worth a second look because it looks like an escape hatch. In a consistent logic the empty type has no closed inhabitants, so a function ⊥ → A can be defined without producing an A. Implementations either provide it as a primitive with no runtime behaviour or derive it from the empty type’s eliminator. In a language with general recursion, the same type is inhabited by a non-terminating term, which is the computational face of inconsistency.

Where the correspondence gets complicated

The simple dictionary holds for intuitionistic propositional logic and the simply typed lambda calculus. Extending it to predicate logic requires dependent types, where a proposition can mention a term and a type can depend on a value. Universal quantification becomes a dependent function type and existential quantification a dependent pair; the details are the subject of Dependent Types as Executable Specifications.

Classical logic is the harder case. Adding excluded middle or double-negation elimination gives a logic that is still consistent and still normalising, but the corresponding calculus is not the pure lambda calculus. The usual computational reading is call-by-name with control operators, where a proof of A ∨ ¬A corresponds to a term that captures the current continuation. In that reading the disjunction property fails computationally as well: the term cannot decide which side without being given a continuation to jump to.

The correspondence also constrains what a type system can express. If every well-typed term normalises, the language cannot contain a general recursion operator, because such an operator would give a closed inhabitant of every type, including the empty one. Practical languages either accept non-termination and lose the logic, or restrict recursion to structurally decreasing arguments and keep it. This is the tension examined in Termination Checking and the Price of Consistency.

Erasing proofs, keeping computation

One practical consequence deserves emphasis because it changes how programs are written. If a type is a proposition whose proof carries no computational content, the compiler can erase the proof at runtime and keep only the parts that compute. A function whose return type is a proof of an equation can be compiled to a function returning nothing, provided the caller never inspects the proof.

The distinction between data and proof is not syntactic; it is a property of the type. A length-indexed vector’s length index is a proof-relevant natural number if code branches on it, and proof-irrelevant if it is only used to justify a type. Systems that track this distinction, either through an explicit universe of propositions or through erasure analysis, can produce code whose runtime representation matches an untyped implementation while retaining the guarantees at compile time.

None of this requires the programmer to think in derivations. It requires that the type checker and the proof checker agree on what a proof is, which is the same requirement as agreeing on what a term of a given type is. That agreement is the content of the correspondence, and it is why a type checker is a proof checker with different surface syntax.