You are previewing Lambda Calculus with Types.
O'Reilly logo
Lambda Calculus with Types

Book Description

This handbook with exercises reveals in formalisms, hitherto mainly used for hardware and software design and verification, unexpected mathematical beauty. The lambda calculus forms a prototype universal programming language, which in its untyped version is related to Lisp, and was treated in the first author's classic The Lambda Calculus (1984). The formalism has since been extended with types and used in functional programming (Haskell, Clean) and proof assistants (Coq, Isabelle, HOL), used in designing and verifying IT products and mathematical proofs. In this book, the authors focus on three classes of typing for lambda terms: simple types, recursive types and intersection types. It is in these three formalisms of terms and types that the unexpected mathematical beauty is revealed. The treatment is authoritative and comprehensive, complemented by an exhaustive bibliography, and numerous exercises are provided to deepen the readers' understanding and increase their confidence using types.

Table of Contents

  1. Cover
  2. Half Title
  3. Perspectives
  4. Title
  5. Copyright
  6. Contents
  7. Preface
  8. Contributors
  9. Our Founders
  10. Introduction
  11. PART I SIMPLE TYPES
    1. 1 The Simply Typed Lambda Calculus
      1. 1.1 The systems
      2. 1.2 First properties and comparisons
      3. 1.3 Normal inhabitants
      4. 1.4 Representing data types
      5. 1.5 Exercises
    2. 2 Properties
      1. 2.1 Normalization
      2. 2.2 Proofs of strong normalization
      3. 2.3 Checking and finding types
      4. 2.4 Checking inhabitation
      5. 2.5 Exercises
    3. 3 Tools
      1. 3.1 Semantics of
      2. 3.2 Lambda theories and term models
      3. 3.3 Syntactic and semantic logical relations
      4. 3.4 Type reducibility
      5. 3.5 The five canonical term-models
      6. 3.6 Exercises
    4. 4 Definability, unification and matching
      1. 4.1 Undecidability of lambda-definability
      2. 4.2 Undecidability of unification
      3. 4.3 Decidability of matching of rank
      4. 4.4 Decidability of the maximal theory
      5. 4.5 Exercises
    5. 5 Extensions
      1. 5.1 Lambda delta
      2. 5.2 Surjective pairing
      3. 5.3 Gödel’s system T: higher-order primitive recursion
      4. 5.4 Spector’s system B: bar recursion
      5. 5.5 Platek’s system Y: fixed point recursion
      6. 5.6 Exercises
    6. 6 Applications
      1. 6.1 Functional programming
      2. 6.2 Logic and proof-checking
      3. 6.3 Proof theory
      4. 6.4 Grammars, terms and types
  12. PART II RECURSIVE TYPES
    1. 7 The Systems
      1. 7.1 Type algebras and type assignment
      2. 7.2 More on type algebras
      3. 7.3 Recursive types via simultaneous recursion
      4. 7.4 Recursive types via µ-abstraction
      5. 7.5 Recursive types as trees
      6. 7.6 Special views on trees
      7. 7.7 Exercises
    2. 8 Properties of Recursive Types
      1. 8.1 Simultaneous recursions vs µ-types
      2. 8.2 Properties of µ-types
      3. 8.3 Properties of types defined by a simultaneous recursion
      4. 8.4 Exercises
    3. 9 Properties of Terms with Types
      1. 9.1 First properties of
      2. 9.2 Finding and inhabiting types
      3. 9.3 Strong normalization
      4. 9.4 Exercises
    4. 10 Models
      1. 10.1 Interpretations of type assignments in
      2. 10.2 Interpreting and
      3. 10.3 Type interpretations in systems with explicit typing
      4. 10.4 Exercises
    5. 11 Applications
      1. 11.1 Subtyping
      2. 11.2 The principal type structures
      3. 11.3 Recursive types in programming languages
      4. 11.4 Further reading
      5. 11.5 Exercises
  13. PART III INTERSECTION TYPES
    1. 12 An Example System
      1. 12.1 The type assignment system ∩BCD
      2. 12.2 The filter model FBCD
      3. 12.3 Completeness of type assignment
    2. 13 Type Assignment Systems
      1. 13.1 Type theories
      2. 13.2 Type assignment
      3. 13.3 Type structures
      4. 13.4 Filters
      5. 13.5 Exercises
    3. 14 Basic Properties of Intersection Type Assignment
      1. 14.1 Inversion lemmas
      2. 14.2 Subject reduction and expansion
      3. 14.3 Exercises
    4. 15 Type and Lambda Structures
      1. 15.1 Meet semi-lattices and algebraic lattices
      2. 15.2 Natural type structures and lambda structures
      3. 15.3 Type and zip structures
      4. 15.4 Zip and lambda structures
      5. 15.5 Exercises
    5. 16 Filter Models
      1. 16.1 Lambda models
      2. 16.2 Filter models
      3. 16.3 D∞models as filter models
      4. 16.4 Other filter models
      5. 16.5 Exercises
    6. 17 Advanced Properties and Applications
      1. 17.1 Realizability interpretation of types
      2. 17.2 Characterizing syntactic properties
      3. 17.3 Approximation theorems
      4. 17.4 Applications of the approximation theorem
      5. 17.5 Undecidability of inhabitation
      6. 17.6 Exercises
  14. References
  15. Indices
    1. Index of terms
    2. Index of citations
    3. Index of symbols