Foundations for programming languages

Summary of contents

• 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