# Curry-Howard isomorphism

The **Curry-Howard isomorphism** (also known as the **Curry-Howard correspondence** ) is the interpretation of types as logical statements and of terms of a certain type as proofs of the statement belonging to the type; and vice versa. It is named after the mathematicians Haskell Brooks Curry and William Alvin Howard .

## Semi-formal description

The concept of *truth* is exchanged with the concept of *provability* , thus follows the intuitionist understanding of mathematics. A statement is provable if there is a term that has the type that matches the statement.

### Simple joiners

A proof of *conjunction* is a pair of proofs for both and .

Evidence of a *disjunction* is a term from the disjoint union of and , .

Evidence for *implications* is total functions of the type .

The logical negation is usually defined as an abbreviation for , where under the Curry-Howard isomorphism corresponds to the empty type .

### Quantifiers

A universally quantified statement becomes a function where the *type* of function *value* depends on the *value of* the function argument. So here you meet *dependent types* .

The proof of an existentially quantified proposition must yield two things: an element , and a proof for .

## Evidence example

The theorem of the excluded third usually does not apply in constructive logic calculi (if it were valid, every statement would be decidable, which leads to either weakness of expression or inconsistency ). A version with double negation below the universal quantization via statements can, however, be proven by specifying a proof term. We are looking for a proof for any statements

- ,

which under Curry-Howard and with the dissolution of the negation abbreviation a *term* of type

becomes. The lambda expression

represents a term of the desired type, where and the injections are in the two-digit sum type.

## Practical applications

Available and usable evidence assistants / programming languages such as Coq , Epigram, and Agda make use of the Curry-Howard isomorphism by allowing evidence to be specified as programs and statements as types. The type verifier takes on the task of verifying the specified evidence.

## swell

- Simon Thompson: Type Theory and Functional Programming (PDF; 1.3 MB)
- Bengt Nordström, Kent Petersson, Jan M. Smith: Programming in Martin-Löfs Type Theory (PDF; 709 kB)
- Philip Wadler: Propositions as Types (PDF; 261 kB)