Foundations for Programming Languages by John C. Mitchell, MIT Press, 1996.

Part 1 Introduction: model programming languages lambda notation equations, reduction and semantics types and type systems notation and mathematical conventions set-theoretic background syntax and semantics induction. Part 2 The language PCF: syntax of PCF PCF programmes and their semantics PCF reduction and symbolic interpreters PCF programming examples, expressive power and limitations variations and extensions of PCF. Part 3 Universal algebra and algebraic data types: preview of algebraic specification algebras, signatures and terms equations, soundness and completeness homomorphisms and initiality algebraic data types rewrite systems. Part 4 Simply-typed lambda calculus: types terms proof systems Henkin models, soundness and completeness. Part 5 Models of typed lambda calculus: domain-theoretic models and fixed points fixed-point induction computational adequacy and full abstraction recursion-theoretic models partial equivalence relations and recursion. Part 6 Imperative programmes: while programmes operational semantics denotational semantics before-after assertions about while programmes semantics of additional programme constructs. Part 7 Categories and recursive types: Cartesian closed categories Kripke lambda models and functor categories domain models of recursive types. Part 8 Logical relations: introduction to logical relations logical relations over applicative structures proof-theoretic results partial surjections and specific models representation independence generalizations of logical relations. Part 9 Polymorphism and modularity: predicative polymorphic calculus impredicative polymorphism data abstraction and existential types general products, sums and programme modules. Part 10 subtyping and related concepts: simply typed lambda calculus with subtyping records, semantic models of subtyping recursive types and a record model of objects polymorphism with subtype constraints. Part 11 Type inference: introduction to type inference type inference for lambda xxx with type variables type inference with polymorphic declarations.