# Curry-Howard Isomorphism

Presented by Carl Eastlund
Transcribed by Sam Tobin-H.

### Curry-Feys 58

Uses combinators instead of explicit lambda terms

Combinators Axioms of P(=>)
K = \x.\y.x A=> (B => A)
S = \x.\y.\z.(xz)(yz) (A=>(B=>C))=>(A=>B)=>A=>C
Application Modus Ponens

Matthias: What's the correspondence here?

Dave: propositions and types

Matthias: these are the basic axioms of logic

### Howard 69, published 80

#### Implication

logic lambda-calc
 A |- A
x A
 G,A |- B G |- A=>B
x A . M B ) A->B
 G |- A; G |- A=>B G |- B
( M A->B N A ) B
Propositions Types
Proofs Terms

Matthias: Types are propositions about programs

#### Strongly normalizing

( x A . M B ) A->B N A ) B
reduces to
M B [ N A / x A ] B

Cut elimination is equivalent to beta reduction

Why must our language be strongly normalizing?

Ω : A for ANY A, this leads to inconsitency

Matthias: All programs are proofs, but what are they proofs of?

#### Negation

logic lambda-calc
false, ~A := A => false ∅ , A -> ∅
 false A
( abort ∅ ->A M ) A

Felix: how do we get M?

Carl: in unreachable parts of the program

#### Conjunction

logic lambda-calc
 B; A A&B
< M A , N B > AxB
 A&B A
Π 1 : AxB -> A
 A&B B
Π 2 : AxB -> B
Matthias: note the correspondence between introduction and elimination rules. This was the inspiration for parts of HtDP.

#### Disjunction

logic lambda-calc
 A A|B
( inl B M A ) A+B
 B A|B
( inr A M B ) A+B
 G,A |- C; G,B |- C; G |- A|B G |- C
( case T A+B of
inl x A => M C
inr x B => N C )
C

#### What don't we have?

• effects
• A | ~A -- the excluded middle
• ~~A -- double negation
• quantification

#### Constructivism

Truth = Proof = Direct evidence

Neither the excluded middle nor double negation provide a witness

#### Quantification

logic lambda-calc
 (a not in G); G,a in t |- A(a) G |- forall x in t.A(x)
a t . M A(a) ) forall x in t.A(x)
 a in t; G|- forall x in t.A(x) G |- A(a)
( M forall x in t.A(x) a t ) A(a)
 A(a); a in t exists x in t.A(x)
< a t M A(a) > exists x in t.A(x)
 G, a in t, A(a) |- C; G |- exists x in t.A(x) G |- C
( let ( x t , u A ) = M exists x in t.A(x) in N C ) C

### Griffin 90

#### Control operators = Classical logic

The following are the rules for the control operators from Friedman, Felleisen
E[A(M)] → M
E[C(M)] → Mλ z.A(E[z])

This gives us the following types
C : ((α→ false)→ false)→α
which is isomorphic to ~~A => A
A : β→α
which is isomorphic to abort.

With this, we can recover all of classical logic.