Curry–Howard and typed lambda calculus

A typing judgment says that a term has a type under a context of named assumptions. For the simply typed fragment, types are built from fixed base types and function types; we also use Boolean constants and their case operator. To introduce a function, temporarily assume an input of its domain and derive a body of its codomain. Discharging that named assumption creates an abstraction. To apply a function, the supplied argument must have its declared domain type.

The context prevents a proof from using unexplained information. A free variable is an outstanding assumption, while a closed term has none. The same term shape may describe a logical proof or a small program depending on the interpretation of its base types. Type checking verifies a proposed derivation; it does not automatically invent its term. Later claims about termination will apply to this total fragment, not to arbitrary code merely written with function notation.

Applying an abstraction replaces its bound variable by the supplied argument. Substitution must avoid capturing free variables of that argument. For example, substituting a free y for x in an abstraction that already binds y requires first renaming the inner binder. This renaming changes the spelling of a bound name without changing the represented function. Ignoring that step can turn a constant function into an identity function and invalidate both the computation and the corresponding proof transformation.

The substitution lemma connects syntax with typing: if the body is well typed using an assumption of type A, and the replacement has type A in the surrounding context, then the substituted body retains its promised type. This lemma underlies preservation for beta reduction. It is not a statement that every informal replacement of symbols is valid. Dependencies, variable scopes, and annotations determine which substitutions are legitimate, particularly once types themselves begin to depend on terms.

Given a proof of A implying B and a proof of B implying C, introduce a hypothetical A, apply the first proof, then apply the second. Abstracting the hypothetical input yields a proof of A implying C. The constructed term makes the order of use explicit. Reversing the two applications usually fails to type check, even if an informal description merely says to combine the implications. Logical composition therefore has a precise interface rather than an interchangeable sequence of steps.

Reduction removes an introduction immediately followed by its matching elimination. In proof language this simplifies a detour; in program language it computes a result. These views reinforce each other without asserting that every proof system has the same evaluation strategy or proof equality. For example, two functions that return the same Boolean on both inputs may need a separate extensional argument in a theory whose judgmental equality only uses the declared reduction rules. We will keep that distinction when studying identity types.