COVID-19 Update: We are currently shipping orders daily. However, due to transit disruptions in some geographies, deliveries may be delayed. To provide all customers with timely access to content, we are offering 50% off Science and Technology Print & eBook bundle options. Terms & conditions.

Lectures on the Curry-Howard Isomorphism, Volume 149

1st Edition

Authors:
eBook ISBN: 9780080478920
Hardcover ISBN: 9780444520777
Imprint: Elsevier Science
Published Date: 4th July 2006
Page Count: 456
Sales tax will be calculated at check-out Price includes VAT/GST
150.00
131.00
105.00
170.00
119.00
Unavailable
Price includes VAT/GST

Institutional Subscription

Preface

Acknowledgements

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 system T

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

Description

The Curry-Howard isomorphism states an amazing correspondence between systems of formal logic as encountered in proof theory and computational calculi as found in type theory. For instance,
minimal propositional logic corresponds to simply typed lambda-calculus, first-order logic corresponds to dependent types, second-order logic corresponds to polymorphic types, sequent calculus is related to explicit substitution, etc.

The isomorphism has many aspects, even at the syntactic level:
formulas correspond to types, proofs correspond 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---that a constructive proof of an implication is a procedure that transforms
proofs of the antecedent into proofs of the succedent; the Curry-Howard isomorphism gives syntactic representations of such procedures. The Curry-Howard isomorphism also provides theoretical foundations for many modern proof-assistant systems (e.g. Coq).

This book give an introduction to parts of proof theory and related aspects of type theory relevant for the Curry-Howard isomorphism. It can serve as an introduction to any or both of typed lambda-calculus and intuitionistic logic.

Key features

- The Curry-Howard Isomorphism treated as 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

Key Features

· 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

Graduate students, lecturers and researchers in logic and theoretical computer science. Also for graduate students, lecturers and researchers in philosophy and mathematics.

No. of pages:
456
Language:
English
Published:
4th July 2006
Imprint:
Elsevier Science
eBook ISBN:
9780080478920
Hardcover ISBN:
9780444520777