Slides and Online Material

1. The Programming Language Core (Slides)

   A core imperative language, typing rules, induction and recursion, unicity of typing, the typing rules define the language, the semantics of the core language, soundness of the typing rules, operational properties of the semantics, the design of a language core.

2. The Abstraction Principle I (Slides)

   Expression abstractions, the semantics of abstractions, soundness of the typing rules for abstractions, lazy evaluation and the copy rule, eager evaluation, semantics of lazy and eager evaluation, other standard abstractions, recursively defined abstractions.

3. The Abstraction Principle II (Slides)

   Variable declarations, semantics of variables, type-structure abstractions, semantics of type structures, declaration abstractions, the abstraction principle is a record introduction principle,

4. The Parameterization and Correspondence Principles (Slides)

   Expression parameters, semantics of parameter transmission, a copy rule for lazily evaluated parameters, other varieties of parameters, type equivalence, type-structure parameters, the correspondence principle, the semantics of correspondence, parameter lists, the parameterization principle is a lambda abstraction principle.

5. The Qualification Principle (Slides)

   Command blocks, semantics of the command block, scope, semantics of dynamic scoping, extent, declaration blocks, type-structure blocks, object-oriented languages, semantics of dynamically scoped objects, subtyping, the copy rule for blocks, the qualification principle is a record introduction principle.

6. Records and Lambda Abstractions (Slides)

   The desugared programming language, record introduction, lambda abstraction introduction, higher-order programming languages, the semantics of records and lambda abstractions, lazy evaluation semantics, eager evaluation semantics, lazy and eager evaluation combined, lambda abstraction alone, orthogonality, the model of the programming language, the logic of the programming language.

7. On Understanding Types, Data Abstraction, and Polymorphism (Slides)

   From untyped to typed universes, the typed lambda-calculus, universal quantification and generic functions, existential quantification and information hiding, bounded quantification and subtyping.