Lambda-Calculus: Types and Models

 Introduction......Page 5
Substitution and beta-conversion......Page 7
  Simple substitution......Page 8
  Alpha-equivalence and substitution......Page 12
  Beta-conversion......Page 18
  Eta-conversion......Page 24
  Head normal forms......Page 29
  Representable functions......Page 31
  Fixed point combinators......Page 34
  The second fixed point theorem......Page 38
  System D......Page 41
  System D......Page 51
  Typings for normal terms......Page 55
  Typings for normalizable terms......Page 61
Strong normalization......Page 69
I-reduction......Page 70
The I-calculus......Page 72
-reduction......Page 74
  The finite developments theorem......Page 77
  The standardization theorem......Page 81
The Böhm theorem......Page 87
  Combinatory algebras......Page 95
  Extensionality axioms......Page 98
  Curry's equations......Page 101
  Translation of -calculus......Page 105
  Functional models......Page 111
  Spaces of continuous increasing functions......Page 116
  Spaces of initial segments......Page 117
  Applications......Page 125
  Retractions......Page 130
  Qualitative domains and stable functions......Page 135
  Definition of system F types......Page 147
  Typing rules for system F......Page 148
  The strong normalization theorem......Page 153
  Data types in system F......Page 155
  Positive second order quantifiers......Page 161
  Second order predicate calculus......Page 167
  System FA2......Page 174
  Realizability......Page 181
  Data types......Page 184
  Programming in FA2......Page 188
Representable functions in system F......Page 195
  Gödel's -translation......Page 198
  Undecidability of strong normalization......Page 201
  Bibliography......Page 205