Curry-Howard correspondence

Curry-Howard correspondence is simply the corresponding between proof and type system. That is :a proof is a program, the formula it proves is a type for the program.
It relate two fields that seem unrelated: proof theory and computability theory. The previous one contain simply typed lamda caculus, Martin lof and CIC, and so on. The latter one contain pushdown automata, turing machine, and so on.
This wiki page also provide an interesting idea:
________________________
can we imagine a typed version of Turing machine that would behave as a proof system? Typed assembly languages are such an instance of "low-level" model of computation that carries types.
________________________

This correspondence can be considered in two level:

1. at the formula and type level that dont consider the detail of proof system and type system
2. at the proof and program level that consider detail of proof system and type system

At the formula and type level, we has following correspondence:

Logic side	Programming side
	Curry-style typing	Church-style typing
universal quantification	intersection type	dependent product type
existential quantification	union type	dependent sum type
implication	function type
conjunction	product type
disjunction	sum type
true formula	unit type
false formula	bottom type

(*this table come from wikipedia*)

product type is just the tuple notation, and sum type is just like HASKELL sub type constructor, for example:
___________________________

datatype tree = Leaf
             | Node of (int * tree * tree)
______________________________

At the level of proof systems and models of computations,

Logic side	Programming side
Hilbert-style deduction system	type system for combinatory logic
natural deduction	type system for lambda calculus

(*this table come from wikipedia*)

Hilbert system use large numbers of axioms, and little number or even only one rule, the modus ponens.