Students will be able to specify the syntax and semantics of programming-language features in imperative and functional languages, including context-dependent syntax (scope and type-checking) and recursive definitions.
Students will be able to use semantic definitions to prove semantic equivalences and soundness and completeness of operational semantics, and validate program-correctness axioms and rules, using, where appropriate, inductive techniques.
Learning outcomes are assessed by assigning weekly exercises.