Part I. Untyped systems

To rigorously discuss type systems, it is essential to establish clear, precise, and mathematically tractable tools for expressing and reasoning about program syntax and semantics.

Initial focus (chapters 3 & 4):

• Subject: A trivial small language consisting only of numbers and booleans.

• Concepts:

  • Abstract syntax.

  • Inductive definitions.

  • Inductive proofs.

  • Inductive evaluation (operational semantics).

  • The modeling of run-time errors.

Next steps (chapters 5-7):

• Subject: The untyped lambda-calculus (a much more powerful language).

• Concepts: Dealing formally with name binding and substitution.

Introducing type systems (Chapter 8 onwards):

• Chapter 8: Returns to the simple language (numbers and booleans) to introduce the basic concepts of static typing.

• Chapter 9: Extends these concepts to the lambda-calculus.