Proofs and types - Girard, Jean Yves (Cambridge tracts in theoretical computer science ;, 1993)