Lectures on the Curry-Howard Isomorphism

The Curry-Howard isomorphism and the theory of the theory of science. For instance,
minimal propositional logic corresponds to simply typed lambda-calculus, first order logic corresponds to polymorphic types, second-order logic corresponds to polymorphic types, etc.

The isomorphism has many aspects, even at the syntactic level:
formulas correspond to types, proofs corresponds to terms, provability corresponds to inhabitation, proof normalization corresponds to term reduction, etc.

But there is more to the isomorphism than this. For instance, it is an old idea --- due to Brouwer, Kolmogorov, and Heyting --- which is a constructive proof of transformation
proofs of the antecedent into proofs of the succedent; the Curry-Howard isomorphism gives syntactic representations of such procedures. The Curry-Howard isomorphism provides the modern proof-assistant systems (eg Coq).

This book is an introduction to the theory of Curry-Howard isomorphism. It can serve as an introduction to any lambda-calculus and intuitionistic logic.

Key features

- The Curry-Howard Isomorphism treated as a common theme

- Reader-friendly introduction to two complementary subjects: Lambda-calculus and constructive logics

- Thorough study of the connection between calculi and logics

- Elaborate study of classical logics and control operators

- Account of dialogue games for classical and intuitionistic logic

- Theoretical foundations of computer-assisted reasoning

· The Curry-Howard Isomorphism treated as the common theme.
· Reader-friendly introduction to two complementary subjects: lambda-calculus and constructive logics
Thorough study of the connection between calculi and logics.
· Elaborate study of classical logics and control operators.
· Account of dialogue games for classical and intuitionistic logic.
· Theoretical foundations of computer-assisted reasoning

Preface

acknowledgments

1. Typefree lambda-calculus

2. Intuitionistic logic

3. Simply typed lambdacalculus

4. The Curry-Howard isomorphism

5. Proofs as combinators

6. Classical logic and control operators

7. Sequent calculus

8. First-order logic

9. First-order arithmetic

10. Gödel's T system

11. Second-order logic and polymorphism

12. Second-order arithmetic

13. Dependent types

14. Pure type systems and the lambda-cube

A Mathematical Background

B Solutions and hints to selected exercises

Bibliography

index