Lectures on the CurryHoward Isomorphism (Enhanced Edition)

 134,99 €

 134,99 €
Description de l’éditeur
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