Semantics and Program Correctness

Formal characterization of programs. Denotational semantics and fixed-point theories. Proof of program correctness and termination. Algebraic theories of abstract data types. Selected topics in the formalization of concurrent computation.