6.4 An altemative presentation of natural deduction 57 6.5 The Curry-Howard Isomorphism.... 5 6.Reductions in the simply-typed lambda calculus 6.7 A word on Church-Rosser .................... 62 68 Reduction as proof simplification 6 Getting mileage out of the Curry-Howard isomorphism 6.10 Disjunction and sum types.. 65 6.11 Classical logic vs.intuitionistic logic......... 6.12 Classical logic and the Curry-Howard isomorphism........ 69 7 Polymorphism 70 8 Weak and strong normalization 8.1 Definitions 70 8 Weak and strong normalization in typed lambdacalculus 71 9 Type inference 72 9.1 Principal types 73 92 Type templates and type substitutions 74 9.3 Unifiers 75 9.4 The unification algorithm. 76 9.5 The type inference algorithm 78 10 Denotational semantics 9 10.1 Set-theoretic interpretation 102 Soundness 82 10.3 Completeness 84 11 The language PCF 85 11.1 Syntax and typing rules 85 11.2 Axiomatic equivalence 86 6.4 An alternative presentation of natural deduction . . . . . . . . . . 57 6.5 The Curry-Howard Isomorphism . . . . . . . . . . . . . . . . . . 59 6.6 Reductions in the simply-typed lambda calculus . . . . . . . . . . 61 6.7 A word on Church-Rosser . . . . . . . . . . . . . . . . . . . . . 62 6.8 Reduction as proof simplification . . . . . . . . . . . . . . . . . . 63 6.9 Getting mileage out of the Curry-Howard isomorphism . . . . . . 64 6.10 Disjunction and sum types . . . . . . . . . . . . . . . . . . . . . 65 6.11 Classical logic vs. intuitionistic logic . . . . . . . . . . . . . . . . 67 6.12 Classical logic and the Curry-Howard isomorphism . . . . . . . . 69 7 Polymorphism 70 8 Weak and strong normalization 70 8.1 Definitions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 70 8.2 Weak and strong normalization in typed lambda calculus . . . . . 71 9 Type inference 72 9.1 Principal types . . . . . . . . . . . . . . . . . . . . . . . . . . . 73 9.2 Type templates and type substitutions . . . . . . . . . . . . . . . 74 9.3 Unifiers . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 75 9.4 The unification algorithm . . . . . . . . . . . . . . . . . . . . . . 76 9.5 The type inference algorithm . . . . . . . . . . . . . . . . . . . . 78 10 Denotational semantics 79 10.1 Set-theoretic interpretation . . . . . . . . . . . . . . . . . . . . . 80 10.2 Soundness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 82 10.3 Completeness . . . . . . . . . . . . . . . . . . . . . . . . . . . . 84 11 The language PCF 85 11.1 Syntax and typing rules . . . . . . . . . . . . . . . . . . . . . . . 85 11.2 Axiomatic equivalence . . . . . . . . . . . . . . . . . . . . . . . 86 3