Lectures on the Curry-Howard isomorphism / Morten Heine Sørensen, Paweł Urzyczyn.

Format:

Book

Author/Creator:

Sørensen, Morten Heine.

Contributor:

Urzyczyn, Paweł.

Series:

Studies in logic and the foundations of mathematics 0049-237X ; v. 149.

Studies in logic and the foundations of mathematics, 0049-237X ; v. 149

Language:

English

Subjects (All):

Curry-Howard isomorphism.

Lambda calculus.

Proof theory.

Physical Description:

xiv, 442 pages : illustrations ; 24 cm.

Edition:

First edition.

Place of Publication:

Amsterdam ; Boston : Elsevier, 2006.

Contents:

1 Type-free [lambda]-calculus 1

1.1 A gentle introduction 1

1.2 Pre-terms and [lambda]-terms 3

1.3 Reduction 10

1.4 The Church-Rosser theorem 12

1.5 Leftmost reductions are normalizing 14

1.6 Perpetual reductions and the conservation theorem 18

1.7 Expressibility and undecidability 19

2 Intuitionistic logic 27

2.1 The BHK interpretation 28

2.2 Natural deduction 32

2.3 Algebraic semantics of classical logic 34

2.4 Heyting algebras 37

2.5 Kripke semantics 43

2.6 The implicational fragment 47

3 Simply typed [lambda]-calculus 55

3.1 Simply typed [lambda]-calculus a la Curry 56

3.2 Type reconstruction algorithm 60

3.3 Simply typed [lambda]-calculus a la Church 63

3.4 Church versus Curry typing 65

3.5 Normalization 67

3.6 Church-Rosser property 70

3.7 Expressibility 72

4 The Curry-Howard isomorphism 77

4.1 Proofs and terms 77

4.2 Type inhabitation 79

4.3 Not an exact isomorphism 81

4.4 Proof normalization 83

4.5 Sums and products 86

4.6 Prover-skeptic dialogues 89

4.7 Prover-skeptic dialogues with absurdity 94

5 Proofs as combinators 103

5.1 Hilbert style proofs 103

5.2 Combinatory logic 108

5.3 Typed combinators 110

5.4 Combinators versus lambda terms 113

5.5 Extensionality 116

5.6 Relevance and linearity 118

6 Classical logic and control operators 127

6.1 Classical propositional logic 127

6.2 The [lambda][mu]-calculus 132

6.3 Subject reduction, confluence, strong normalization 137

6.4 Logical embedding and CPS translation 140

6.5 Classical prover-skeptic dialogues 144

6.6 The pure implicational fragment 150

6.7 Conjunction and disjunction 153

7 Sequent calculus 161

7.1 Gentzen's sequent calculus LK 162

7.2 Fragments of LK versus natural deduction 165

7.3 Gentzen's Hauptsatz 169

7.4 Cut elimination versus normalization 174

7.5 Lorenzen dialogues 181

8 First-order logic 195

8.1 Syntax of first-order logic 195

8.2 Informal semantics 197

8.3 Proof systems 200

8.4 Classical semantics 205

8.5 Algebraic semantics of intuitionistic logic 207

8.6 Kripke semantics 212

8.7 Lambda-calculus 215

8.8 Undecidability 221

9 First-order arithmetic 229

9.1 The language of arithmetic 229

9.2 Peano Arithmetic 232

9.3 Godel's theorems 234

9.4 Representable and provably recursive functions 237

9.5 Heyting Arithmetic 240

9.6 Kleene's realizability interpretation 243

10 Godel's system T 251

10.1 From Heyting Arithmetic to system T 251

10.2 Syntax 253

10.3 Strong normalization 256

10.4 Modified realizability 260

11 Second-order logic and polymorphism 269

11.1 Propositional second-order logic 270

11.2 Polymorphic lambda-calculus (system F) 276

11.3 Expressive power 280

11.4 Curry-style polymorphism 284

11.5 Strong normalization 287

11.6 The inhabitation problem 290

11.7 Higher-order polymorphism 296

12 Second-order arithmetic 303

12.1 Second-order syntax 303

12.2 Classical second-order logic 305

12.3 Intuitionistic second-order logic 308

12.4 Second-order Peano Arithmetic 311

12.5 Second-order Heyting Arithmetic 314

12.6 Simplified syntax 315

12.7 Lambda-calculus 318

13 Dependent types 325

13.1 The language of [lambda]P 326

13.2 Type assignment 328

13.3 Strong normalization 333

13.4 Dependent types a la Curry 335

13.5 Correspondence with first-order logic 337

14 Pure type systems and the [lambda]-cube 343

14.1 System [lambda]P revisited 343

14.2 Pure type systems 344

14.3 The Calculus of Constructions 346

14.4 Strong normalization 348

14.5 Beyond the cube 351

14.6 Girard's paradox 352

A Mathematical background 361

A.1 Set theory 361

A.2 Algebra and unification 365

A.3 Partial recursive functions 366

A.4 Decision problems 368

A.5 Hard and complete 370

B Solutions and hints to selected exercises 373.

Notes:

Includes bibliographical references (pages 403-430) and index.

ISBN:

0444520775

OCLC:

70158578

Publisher Number:

9780444520777

Online:

Publisher description