This course is a continuation of "Computational Models".

It covers many topics essential to an understanding of programming languages and software verification.

Students helped write up the class notes.
 

Look here for the final exam!

Outline

1. Operational semantics
• Rewriting
• Lambda calculus
• Typed calculi
2. Declarative semantics
• Axiomatic semantics (briefly)
• Type theory
• Algebraic semantics
3. Denotational semantics
• Fixpoint theory
• Recursive programs
• Lambda models

1. Infinite words (omitted)
2. Concurrency
• Basic models
• Interaction