Course Sections

We will cover the following chapters:

1. -calculus
   • syntax
   • semantics

2. Type theory
   • typed -calculus
   • logic
   • program verification

3. Functional programming languages
   • PCF (a theoretical, stripped-down language)
   • ML

4. Semantics
   • Scott theory (denotational semantics)
   • structured operational semantics

5. Imperative programming languages
   • Simple Imperative Language (Gunter)
   • Polya (a complete structural semantics has been developed for this by Stuart Allen)

6. Logic and constraint programming (?)
   • Prolog
   • -Prolog

7. Object-oriented programming
   • record algebra
   • algebra (i.e., groups, rings, and fields, used as a programming example, if the class is sufficiently prepared)