Lectures on the Curry-Howard Isomorphism, Volume 149 (Studies in Logic and the Foundations of Mathematics) Export

@book{citeulike:1584936, abstract = {{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,<br>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.<br><br>The isomorphism has many aspects, even at the syntactic level:<br>formulas correspond to types, proofs correspond to terms, provability corresponds to inhabitation, proof normalization corresponds to term reduction, etc.<br><br>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<br>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).<br><br>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.<P><br><br>Key features<BR><br>- The Curry-Howard Isomorphism treated as common theme<BR><br>- Reader-friendly introduction to two complementary subjects: Lambda-calculus and constructive logics<BR><br>- Thorough study of the connection between calculi and logics<BR><br>- Elaborate study of classical logics and control operators<BR><br>- Account of dialogue games for classical and intuitionistic logic<BR><br>- Theoretical foundations of computer-assisted reasoning<P><br><br>· The Curry-Howard Isomorphism treated as the common theme.<br>· Reader-friendly introduction to two complementary subjects: lambda-calculus and constructive logics <br>· Thorough study of the connection between calculi and logics.<br>· Elaborate study of classical logics and control operators.<br>· Account of dialogue games for classical and intuitionistic logic.<br>· Theoretical foundations of computer-assisted reasoning}}, author = {S{\o}rensen, Morten H. and Urzyczyn, Pawel}, citeulike-article-id = {1584936}, citeulike-linkout-0 = {http://www.amazon.ca/exec/obidos/redirect?tag=citeulike09-20&amp;path=ASIN/0444520775}, citeulike-linkout-1 = {http://www.amazon.de/exec/obidos/redirect?tag=citeulike01-21&amp;path=ASIN/0444520775}, citeulike-linkout-2 = {http://www.amazon.fr/exec/obidos/redirect?tag=citeulike06-21&amp;path=ASIN/0444520775}, citeulike-linkout-3 = {http://www.amazon.co.uk/exec/obidos/ASIN/0444520775/citeulike00-21}, citeulike-linkout-4 = {http://www.amazon.com/exec/obidos/redirect?tag=citeulike07-20&path=ASIN/0444520775}, citeulike-linkout-5 = {http://www.worldcat.org/isbn/0444520775}, citeulike-linkout-6 = {http://books.google.com/books?vid=ISBN0444520775}, citeulike-linkout-7 = {http://www.amazon.com/gp/search?keywords=0444520775&index=books&linkCode=qs}, citeulike-linkout-8 = {http://www.librarything.com/isbn/0444520775}, day = {14}, howpublished = {Hardcover}, isbn = {0444520775}, keywords = {curry-howard, intuitionistic, logic}, month = {September}, posted-at = {2007-08-23 08:48:42}, priority = {0}, publisher = {{Elsevier Science}}, title = {Lectures on the Curry-Howard Isomorphism, Volume 149 (Studies in Logic and the Foundations of Mathematics)}, url = {http://www.amazon.com/exec/obidos/redirect?tag=citeulike07-20&path=ASIN/0444520775}, year = {2006} }

TY - BOOK ID - citeulike:1584936 L3 - citeulike-article-id:1584936 N2 - {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,<br>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.<br><br>The isomorphism has many aspects, even at the syntactic level:<br>formulas correspond to types, proofs correspond to terms, provability corresponds to inhabitation, proof normalization corresponds to term reduction, etc.<br><br>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<br>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).<br><br>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.<P><br><br>Key features<BR><br>- The Curry-Howard Isomorphism treated as common theme<BR><br>- Reader-friendly introduction to two complementary subjects: Lambda-calculus and constructive logics<BR><br>- Thorough study of the connection between calculi and logics<BR><br>- Elaborate study of classical logics and control operators<BR><br>- Account of dialogue games for classical and intuitionistic logic<BR><br>- Theoretical foundations of computer-assisted reasoning<P><br><br>· The Curry-Howard Isomorphism treated as the common theme.<br>· Reader-friendly introduction to two complementary subjects: lambda-calculus and constructive logics <br>· Thorough study of the connection between calculi and logics.<br>· Elaborate study of classical logics and control operators.<br>· Account of dialogue games for classical and intuitionistic logic.<br>· Theoretical foundations of computer-assisted reasoning} SN - 0444520775 TI - Lectures on the Curry-Howard Isomorphism, Volume 149 (Studies in Logic and the Foundations of Mathematics) PB - {Elsevier Science} KW - curry-howard KW - intuitionistic KW - logic AU - Sørensen, Morten AU - Urzyczyn, Pawel PY - 2006/09/14/ UR - http://www.amazon.ca/exec/obidos/redirect?tag=citeulike09-20&amp;path=ASIN/0444520775 ER -