# Curry howard isomorphism “proof as program”

I'm reading CH Isomorphism.

Let's divide into two stages:

1. Prop corresponds to types. so a proposition A $\wedge$ B corresponds to type A $\times$ B.

2. Proof corresponds to the program. What is the corresponding proof and program in this case ?

As far as I can guess the proof is a pair but how we denote program ? Is that a lambda term "pair" ?? What we mean by a proof here. coz proof is a complete derivation in case a pro example exists ?? Very confused . Can someone help ?

• see en.m.wikipedia.org/wiki/Brouwer–Heyting–Kolmogorov_interpretation – user48832 Oct 30 '16 at 23:14
• sorry that link paste did not work. Google "Brouwer–Heyting–Kolmogorov interpretation" – user48832 Oct 30 '16 at 23:16
• Thanks. i think now i understand (i think) the proof part. Can you comment on program part. – Pushpa Oct 31 '16 at 4:46
• a proof is a program. it's weird at first. the trick is to see that in classic truth-conditional (TC) logic, a proof just involves true propositions like by truth tables. they show, they don't do. in constructive logic, proofs do, they don't show. put differently, in constructive logic we have no need for the concept "true". to say that P is true is just a convenient way of saying that we can construct something whose type is P. – user48832 Oct 31 '16 at 19:13
• Yeah now soaking it up. A is true is a judgment which means we have the evidence that A is true. If we consider proof as tree and program as lambda terms evrything make sense, But then things gets messy when they(Frank Pfenning @cmu) talks about "proof term". Is proof term is term in lambda calculus ?? for example <u,v> : A ∧ B what is this pair <u,v> ?? If this is a lambda term ? What proof term is then ? – Pushpa Nov 1 '16 at 5:24