Presented by Carl Eastlund
Transcribed by Sam TobinH.
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
logic  lambdacalc  


x ^{ A }  

(λ x ^{ A } . M ^{ B } ) ^{ A>B }  

( M ^{ A>B } N ^{ A } ) ^{ B }  
Propositions  Types  
Proofs  Terms 
Matthias: Types are propositions about programs
(
(λ
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?
logic  lambdacalc  

false, ~A := A => false  ∅ , A > ∅  

( abort ^{ ∅ >A } M ^{∅ } ) ^{ A } 
Felix: how do we get M?
Carl: in unreachable parts of the program
logic  lambdacalc  


< M ^{ A } , N ^{ B } > ^{ AxB }  

Π _{ 1 } : AxB > A  

Π _{ 2 } : AxB > B 
logic  lambdacalc  


( inl ^{ B } M ^{ A } ) ^{ A+B }  

( inr ^{ A } M ^{ B } ) ^{ A+B }  

(
case
T
^{
A+B
}
of
inl x ^{ A } => M ^{ C } inr x ^{ B } => N ^{ C } ) ^{ C } 
Truth = Proof = Direct evidence
Neither the excluded middle nor double negation provide a witness
logic  lambdacalc  


(λ a ^{ t } . M ^{ A(a) } ) ^{ forall x in t.A(x) }  

( M ^{ forall x in t.A(x) } a ^{ t } ) ^{ A(a) }  

< a ^{ t } M ^{ A(a) } > ^{ exists x in t.A(x) }  

( let ( x ^{ t } , u ^{ A } ) = M ^{ exists x in t.A(x) } in N ^{ C } ) ^{ C } 
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.