Lectures on the Curry-Howard Isomorphism.

By: Sørensen, Morten HeineContributor(s): Urzyczyn, Pawel | Sorensen, Morten HeineSeries: Issn SerPublisher: Oxford : Elsevier Science & Technology, 2006Copyright date: ©2006Edition: 1st edDescription: 1 online resource (457 pages)Content type: text Media type: computer Carrier type: online resourceISBN: 9780080478920Subject(s): Lambda calculusGenre/Form: Electronic books. Additional physical formats: Print version:: Lectures on the Curry-Howard IsomorphismDDC classification: 511.326 LOC classification: QA9.54.S67 2006Online resources: Click to View
Contents:
Cover -- Lectures on the curry-howard isomorphism -- Copyright -- Preface -- Contents -- Chapter 1 Type-free λ-calculus -- 1.1 A gentle introduction -- 1.2 Pre-terms and λ-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 undecidability -- 1.8 Notes -- 1.9 Exercises -- Chapter 2 Intuitionistic 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 -- Chapter 3 Simply typed λ-calculus -- 3.1 Simply typed λ-calculus à la Curry -- 3.2 Type reconstruction algorithm -- 3.3 Simply typed λ-calculus à 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 -- 5.1 Hilbert style proofs -- 5.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 propositional logic -- 6.2 The λμ-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 -- 7.2 Fragments of LK versus natural deduction -- 7.3 Gentzen's Hauptsatz -- 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 intuitionistic logic -- 8.6 Kripke semantics -- 8.7 Lambda-calculus -- 8.8 Undecidability -- 8.9 Notes -- 8.10 Exercises -- Chapter 9 First-order arithmetic -- 9.1 The language of arithmetic -- 9.2 Peano Arithmetic -- 9.3 Gödel's theorems -- 9.4 Representable and provably recursive functions -- 9.5 Heyting Arithmetic -- 9.6 Kleene's realizability interpretation -- 9.7 Notes -- 9.8 Exercises -- Chapter 10 Gödel'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 Propositional second-order logic -- 11.2 Polymorphic lambda-calculus (system F) -- 11.3 Expressive power -- 11.4 Curry-style polymorphism -- 11.5 Strong normalization -- 11.6 The inhabitation problem -- 11.7 Higher-order polymorphism -- 11.8 Notes -- 11.9 Exercises -- Chapter 12 Second-order arithmetic -- 12.1 Second-order syntax -- 12.2 Classical second-order logic -- 12.3 Intuitionistic second-order logic -- 12.4 Second-order Peano Arithmetic -- 12.5 Second-order Heyting Arithmetic -- 12.6 Simplified syntax -- 12.7 Lambda-calculus -- 12.8 Notes -- 12.9 Exercises -- Chapter 13 Dependent types -- 13.1 The language of λP -- 13.2 Type assignment -- 13.3 Strong normalization -- 13.4 Dependent types à la Curry -- 13.5 Correspondence with first-order logic -- 13.6 Notes -- 13.7 Exercises -- Chapter 14 Pure type systems and the λ-cube -- 14.1 System λP revisited.
14.2 Pure type systems -- 14.3 The Calculus of Constructions -- 14.4 Strong normalization -- 14.5 Beyond the cube -- 14.6 Girard's paradox -- 14.7 Notes -- 14.8 Exercises -- Appendix A Mathematical background -- A.1 Set theory -- A.2 Algebra and unification -- A.3 Partial recursive functions -- A.4 Decision problems -- A.5 Hard and complete -- Appendix B Solutions and hints to selected exercises -- Solutions to Chapter 1 -- Solutions to Chapter 2 -- Solutions to Chapter 3 -- Solutions to Chapter 4 -- Solutions to Chapter 5 -- Solutions to Chapter 6 -- Solutions to Chapter 7 -- Solutions to Chapter 8 -- Solutions to Chapter 9 -- Solutions to Chapter 10 -- Solutions to Chapter 11 -- Solutions to chapter 12 -- Solutions to Chapter 13 -- Solutions to Chapter 14 -- Bibliography -- Index.
Summary: 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:Summary: 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.
Holdings
Item type Current library Call number Status Date due Barcode Item holds
Ebrary Ebrary Afghanistan
Available EBKAF00016962
Ebrary Ebrary Algeria
Available
Ebrary Ebrary Cyprus
Available
Ebrary Ebrary Egypt
Available
Ebrary Ebrary Libya
Available
Ebrary Ebrary Morocco
Available
Ebrary Ebrary Nepal
Available EBKNP00016962
Ebrary Ebrary Sudan

Access a wide range of magazines and books using Pressreader and Ebook central.

Enjoy your reading, British Council Sudan.

Available
Ebrary Ebrary Tunisia
Available
Total holds: 0

Cover -- Lectures on the curry-howard isomorphism -- Copyright -- Preface -- Contents -- Chapter 1 Type-free λ-calculus -- 1.1 A gentle introduction -- 1.2 Pre-terms and λ-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 undecidability -- 1.8 Notes -- 1.9 Exercises -- Chapter 2 Intuitionistic 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 -- Chapter 3 Simply typed λ-calculus -- 3.1 Simply typed λ-calculus à la Curry -- 3.2 Type reconstruction algorithm -- 3.3 Simply typed λ-calculus à 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 -- 5.1 Hilbert style proofs -- 5.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 propositional logic -- 6.2 The λμ-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 -- 7.2 Fragments of LK versus natural deduction -- 7.3 Gentzen's Hauptsatz -- 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 intuitionistic logic -- 8.6 Kripke semantics -- 8.7 Lambda-calculus -- 8.8 Undecidability -- 8.9 Notes -- 8.10 Exercises -- Chapter 9 First-order arithmetic -- 9.1 The language of arithmetic -- 9.2 Peano Arithmetic -- 9.3 Gödel's theorems -- 9.4 Representable and provably recursive functions -- 9.5 Heyting Arithmetic -- 9.6 Kleene's realizability interpretation -- 9.7 Notes -- 9.8 Exercises -- Chapter 10 Gödel'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 Propositional second-order logic -- 11.2 Polymorphic lambda-calculus (system F) -- 11.3 Expressive power -- 11.4 Curry-style polymorphism -- 11.5 Strong normalization -- 11.6 The inhabitation problem -- 11.7 Higher-order polymorphism -- 11.8 Notes -- 11.9 Exercises -- Chapter 12 Second-order arithmetic -- 12.1 Second-order syntax -- 12.2 Classical second-order logic -- 12.3 Intuitionistic second-order logic -- 12.4 Second-order Peano Arithmetic -- 12.5 Second-order Heyting Arithmetic -- 12.6 Simplified syntax -- 12.7 Lambda-calculus -- 12.8 Notes -- 12.9 Exercises -- Chapter 13 Dependent types -- 13.1 The language of λP -- 13.2 Type assignment -- 13.3 Strong normalization -- 13.4 Dependent types à la Curry -- 13.5 Correspondence with first-order logic -- 13.6 Notes -- 13.7 Exercises -- Chapter 14 Pure type systems and the λ-cube -- 14.1 System λP revisited.

14.2 Pure type systems -- 14.3 The Calculus of Constructions -- 14.4 Strong normalization -- 14.5 Beyond the cube -- 14.6 Girard's paradox -- 14.7 Notes -- 14.8 Exercises -- Appendix A Mathematical background -- A.1 Set theory -- A.2 Algebra and unification -- A.3 Partial recursive functions -- A.4 Decision problems -- A.5 Hard and complete -- Appendix B Solutions and hints to selected exercises -- Solutions to Chapter 1 -- Solutions to Chapter 2 -- Solutions to Chapter 3 -- Solutions to Chapter 4 -- Solutions to Chapter 5 -- Solutions to Chapter 6 -- Solutions to Chapter 7 -- Solutions to Chapter 8 -- Solutions to Chapter 9 -- Solutions to Chapter 10 -- Solutions to Chapter 11 -- Solutions to chapter 12 -- Solutions to Chapter 13 -- Solutions to Chapter 14 -- Bibliography -- Index.

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.

Description based on publisher supplied metadata and other sources.

Electronic reproduction. Ann Arbor, Michigan : ProQuest Ebook Central, 2019. Available via World Wide Web. Access may be limited to ProQuest Ebook Central affiliated libraries.

There are no comments on this title.

to post a comment.