Derivation and Computation : Taking the Curry-Howard Correspondence Seriously (Hardcover)

Introduction; Preview; Part I. Development and Exercises: 1. Derivation systems; 2. Computation mechanisms; 3. The typed combinator calculus; 4. The typed l-calculus; 5. Substitution algorithms; 6. Applied l-calculi; 7. Multi-recursive arithmetic; 8. Ordinals and ordinal notation; 9. Higher order recursion; Part II. Solutions: A. Derivation systems; B. Computation mechanisms; C. The typed combinator calculus; D. The typed l-calculus; E. Substitution algorithms; F. Applied l-calculi; G. Multi-recursive arithmetic; H. Ordinals and ordinal notation; I. Higher order recursion; Postview; Bibliography; Commonly used symbols; Index.