Programming languages are a fundamental part of computer science. This course
introduces the formal tools needed to describe precisely what a program means.
These tools help us answer many useful questions about program analyses and
transformations, such as:
- Is this program is correct?
- Will this program encounter a run-time type error?
- Is one program indistinguishable from another?
- Is this optimization a safe program transformation?
- Can programs written in this language crash?
- Is this compiler translation correct?
- Can source language A be translated into target language B?
- Different styles of dynamic semantics, including operational, axiomatic,
and denotational semantics
- Static semantics, including type systems
- Proofs by induction on derivations and structure
- A formal treatment of important programming language features such as
functions, laziness, exceptions, continuations, modules, type polymorphism, objects