According to Curry-Howard correspondence, types are conclusions and programs are proofs of the conclusion. Any program is corresponded to a deduction procedure, such as a Hilbert-style proof or natural deduction proof.