LEADER 00000cam a2200661Ia 4500 
001    ocn162586983 
003    OCoLC 
005    20160527041114.5 
006    m     o  d         
007    cr cn||||||||| 
008    070806s2006    ne a    ob    001 0 eng d 
016 7  013464440|2Uk 
019    154225201|a441806456|a648299514|a779919943 
020    9780444520777 
020    0444520775 
020    9780080478920|q(electronic book) 
020    0080478921|q(electronic book) 
035    (OCoLC)162586983|z(OCoLC)154225201|z(OCoLC)441806456
       |z(OCoLC)648299514|z(OCoLC)779919943 
037    116411:116509|bElsevier Science & Technology|nhttp://
       www.sciencedirect.com 
040    OPELS|beng|epn|cOPELS|dOPELS|dOCLCQ|dN$T|dYDXCP|dMERUC
       |dE7B|dIDEBK|dREDDC|dOCLCO|dOCLCQ|dDEBSZ|dOPELS|dOCLCF
       |dDEBBG|dTULIB|dOCLCQ|dEBLCP|dOCLCQ|dCOO|dOCLCQ 
049    RIDW 
050  4 QA9.54|b.S67 2006eb 
072  7 MAT|x031000|2bisacsh 
082 04 511.3/26|222 
090    QA9.54|b.S67 2006eb 
100 1  Sørensen, Morten Heine.|0https://id.loc.gov/authorities/
       names/n2006046636 
245 10 Lectures on the Curry-Howard isomorphism /|cMorten Heine 
       Sørensen, Paweł Urzyczyn. 
250    1st ed. 
264  1 Amsterdam ;|aBoston [MA] :|bElsevier,|c2006. 
300    1 online resource (xiv, 442 pages) :|billustrations. 
336    text|btxt|2rdacontent 
337    computer|bc|2rdamedia 
338    online resource|bcr|2rdacarrier 
340    |gpolychrome|2rdacc 
347    text file|2rdaft 
490 1  Studies in logic and the foundations of mathematics,|x0049
       -237X ;|vv. 149 
504    Includes bibliographical references (pages 403-430) and 
       index. 
505 0  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. 
520    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 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. 
588 0  Print version record. 
590    eBooks on EBSCOhost|bEBSCO eBook Subscription Academic 
       Collection - North America 
650  0 Curry-Howard isomorphism.|0https://id.loc.gov/authorities/
       subjects/sh2001002954 
650  0 Lambda calculus.|0https://id.loc.gov/authorities/subjects/
       sh85074174 
650  0 Proof theory.|0https://id.loc.gov/authorities/subjects/
       sh85107437 
650  7 Curry-Howard isomorphism.|2fast|0https://id.worldcat.org/
       fast/885411 
650  7 Lambda calculus.|2fast|0https://id.worldcat.org/fast/
       991011 
650  7 Proof theory.|2fast|0https://id.worldcat.org/fast/1078942 
655  4 Electronic books. 
700 1  Urzyczyn, Paweł.|0https://id.loc.gov/authorities/names/
       nb2005005743 
776 08 |iPrint version:|aSørensen, Morten Heine.|tLectures on the
       Curry-Howard isomorphism.|b1st ed.|dAmsterdam ; Boston 
       [MA] : Elsevier, 2006|z0444520775|z9780444520777|w(DLC)  
       2006048390|w(OCoLC)70158578 
830  0 Studies in logic and the foundations of mathematics ;
       |0https://id.loc.gov/authorities/names/n42707789|vv. 149.
       |x0049-237X 
856 40 |uhttps://rider.idm.oclc.org/login?url=http://
       search.ebscohost.com/login.aspx?direct=true&scope=site&
       db=nlebk&AN=196231|zOnline eBook. Access restricted to 
       current Rider University students, faculty, and staff. 
856 42 |3Instructions for reading/downloading this eBook|uhttp://
       guides.rider.edu/ebooks/ebsco 
901    MARCIVE 20231220 
948    |d20160615|cEBSCO|tebscoebooksacademic|lridw 
994    92|bRID