CMSC 731 - Semantics of Programming Languages

[3]

The fundamentals of axiomatic and denotational semantics, their corresponding techniques for program specification and verification. Axiomatic methods include Hoare’s logic and Dijkstra’s predicate transformers. Denotational methods include fixpoint theory and an introduction to the lambda calculus. Denotational methods are used to prove the soundness of selected axiomatic proof rules.
Prerequisite: Prerequisite: CMSC 631 or consent of instructor.