I'm reading CH Isomorphism. Let's divide into two stages:Prop corresponds to types. so a proposition A $\wedge$ B corresponds to type A $\times$ B. 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 ?
Curry howard isomorphism proof as program
type theory;curry howard