Formal approaches to defining semantics of programming languages: denotational, operational, axiomatic, and transformational semantics. Formal systems for program verification. Logics of program, type theory, lambda calculus. Further topics selected from term rewriting approach to proving properties of data types, and semantics and verification of languages with concurrent and parallel constructs.