LEADER 05587nam 2200697Ia 450 001 9910784595103321 005 20200520144314.0 010 $a1-281-05105-5 010 $a9786611051051 010 $a0-08-047892-1 035 $a(CKB)1000000000357888 035 $a(EBL)294228 035 $a(OCoLC)469589380 035 $a(SSID)ssj0000190882 035 $a(PQKBManifestationID)11185057 035 $a(PQKBTitleCode)TC0000190882 035 $a(PQKBWorkID)10180812 035 $a(PQKB)10018668 035 $a(Au-PeEL)EBL294228 035 $a(CaPaEBR)ebr10185917 035 $a(CaONFJC)MIL105105 035 $a(MiAaPQ)EBC294228 035 $a(EXLCZ)991000000000357888 100 $a20060607d2006 uy 0 101 0 $aeng 135 $aur|n|---||||| 181 $ctxt 182 $cc 183 $acr 200 10$aLectures on the Curry-Howard isomorphism$b[electronic resource] /$fMorten Heine Sørensen, Pawe? Urzyczyn 205 $a1st ed. 210 $aAmsterdam ;$aBoston [MA] $cElsevier$d2006 215 $a1 online resource (457 p.) 225 1 $aStudies in logic and the foundations of mathematics,$x0049-237X ;$vv. 149 300 $aDescription based upon print version of record. 311 $a0-444-52077-5 320 $aIncludes bibliographical references (p. 403-430) and index. 327 $aCover; Title Page; Copyright Page; Table of Contents; Chapter 1 Type-free Lambda-calculus; 1.1 A gentle introduction; 1.2 Pre-terms and Lambda-terms; 1.3 Reduction; 1.4 The Church-Rosser theorem; 1.5 Leftmost reductions are normalizing; 1.6 Perpetual reductions and the conservation theorem; 1.7 Expressibility and undeeidability; 1.8 Notes; 1.9 Exercises; Chapter 2 Intultionistic logic; 2.1 The BHK interpretation; 2.2 Natural deduction; 2.3 Algebraic semantics of classical logic; 2.4 Heyting algebras; 2.5 Kripke semantics; 2.6 The implicational fragment; 2.7 Notes; 2.8 Exercises 327 $aChapter 3 Simply typed Lambda-calcuIus3.1 Simply typed Lambda-ealculus a la Curry; 3.2 Type reconstruction algorithm; 3.3 Simply typed Lambda-calculus a la Church; 3.4 Church versus Curry typing; 3.5 Normalization; 3.6 Church-Rosser property; 3.7 Expressibility; 3.8 Notes; 3.9 Exercises; Chapter 4 The Curry-Howard isomorphism; 4.1 Proofs and terms; 4.2 Type inhabitation; 4.3 Not an exact isomorphism; 4.4 Proof normalization; 4.5 Sums and products; 4.6 Prover-skeptic dialogues; 4.7 Prover-skeptic dialogues with absurdity; 4.8 Notes; 4.9 Exercises; Chapter 5 Proofs as combinators 327 $a5.1 Hubert style proofs5.2 Combinatory logic; 5.3 Typed combinators; 5.4 Combinators versus lambda terms; 5.5 Extensionality; 5.6 Relevance and linearity; 5.7 Notes; 5.8 Exercises; Chapter 6 Classical logic and control operators; 6.1 Classical prepositional lope; 6.2 The Lambda meu-calculus; 6.3 Subject reduction, confluence, strong normalization; 6.4 Logical embedding and CPS translation; 6.5 Classical prover-skeptic dialogues; 6.6 The pure implicational fragment; 6.7 Conjunction and disjunction; 6.8 Notes; 6.9 Exercises; Chapter 7 Sequent calculus; 7.1 Gentzen's sequent calculus LK 327 $a7.2 Fragments of LK versus natural deduction7.3 Gentzen's Hauptaatz; 7.4 Cut elimination versus normalization; 7.5 Lorenzen dialogues; 7.6 Notes; 7.7 Exercises; Chapter 8 First-order logic; 8.1 Syntax of first-order logic; 8.2 Informal semantics; 8.3 Proof systems; 8.4 Classical semantics; 8.5 Algebraic semantics of intuitionistie logic; 8.6 Kripke semantics; 8.7 Lambda-calculus; 8.8 Undeddability; 8.9 Notes; 8.10 Exercises; Chapter 9 First-order arithmetic; 9.1 The language of arithmetic; 9.2 Peano Arithmetic; 9.3 Godel's theorems; 9.4 Representable and provably recursive functions 327 $a9.5 Heyting Arithmetic9.6 Kleene's realfeability interpretation; 9.7 Notes; 9.8 Exercises; Chapter 10 Godel's system T; 10.1 From Heyting Arithmetic to system T; 10.2 Syntax; 10.3 Strong normalization; 10.4 Modified realizability; 10.5 Notes; 10.6 Exercises; Chapter 11 Second-order logic and polymorphism; 11.1 Prepositional second-order logic; 11.2 Polymorphic lambda-calculus (system F); 11.3 Expressive power; 11.4 Gurry-style polymorphism; 11.5 Strong normalization; 11.6 The inhabitation problem; 11.7 Higher-order polymorphism; 11.8 Notes; 11.9 Exercises 327 $aChapter 12 Second-order arithmetic 330 $aThe 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, 410 0$aStudies in logic and the foundations of mathematics ;$vv. 149. 606 $aCurry-Howard isomorphism 606 $aLambda calculus 606 $aProof theory 615 0$aCurry-Howard isomorphism. 615 0$aLambda calculus. 615 0$aProof theory. 676 $a511.3/26 700 $aSørensen$b Morten Heine$0433380 701 $aUrzyczyn$b Pawe?$0318886 801 0$bMiAaPQ 801 1$bMiAaPQ 801 2$bMiAaPQ 906 $aBOOK 912 $a9910784595103321 996 $aLectures on the Curry-Howard isomorphism$9728350 997 $aUNINA