Edition 
1st ed. 
Description 
1 online resource (xiv, 442 pages) : illustrations. 
Series 
Studies in logic and the foundations of mathematics,
0049237X ;
v. 149


Studies in logic and the foundations of mathematics ; v. 149.
0049237X

Summary 
The CurryHoward 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 lambdacalculus, firstorder logic corresponds to dependent types, secondorder 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 ideadue to Brouwer, Kolmogorov, and Heytingthat a constructive proof of an implication is a procedure that transforms proofs of the antecedent into proofs of the succedent; the CurryHoward isomorphism gives syntactic representations of such procedures. The CurryHoward isomorphism also provides theoretical foundations for many modern proofassistant systems (e.g. Coq). This book give an introduction to parts of proof theory and related aspects of type theory relevant for the CurryHoward isomorphism. It can serve as an introduction to any or both of typed lambdacalculus and intuitionistic logic. Key features  The CurryHoward Isomorphism treated as common theme  Readerfriendly introduction to two complementary subjects: Lambdacalculus 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 computerassisted reasoning The CurryHoward Isomorphism treated as the common theme. Readerfriendly introduction to two complementary subjects: lambdacalculus 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 computerassisted reasoning. 
Contents 
Preface  Acknowledgements  1. Typefree lambdacalculus  2. Intuitionistic logic  3. Simply typed lambdacalculus  4. The CurryHoward isomorphism  5. Proofs as combinators  6. Classical logic and control operators  7. Sequent calculus  8. Firstorder logic  9. Firstorder arithmetic  10. G̲del's system T  11. Secondorder logic and polymorphism  12. Secondorder arithmetic  13. Dependent types  14. Pure type systems and the lambdacube  A Mathematical Background  B Solutions and hints to selected exercises  Bibliography  Index. 
Bibliography 
Includes bibliographical references (pages 403430) and index. 
Local Note 
eBooks on EBSCOhost EBSCO eBook Subscription Academic Collection  North America 
Subject 
CurryHoward isomorphism.


Lambda calculus.


Proof theory.

Genre/Form 
Electronic books.

Added Author 
Urzyczyn, Paweł.

Other Form: 
Print version: Sørensen, Morten Heine. Lectures on the CurryHoward isomorphism. 1st ed. Amsterdam ; Boston [MA] : Elsevier, 2006 0444520775 9780444520777 (DLC) 2006048390 (OCoLC)70158578 
ISBN 
9780444520777 

0444520775 

9780080478920 (electronic bk.) 

0080478921 (electronic bk.) 
