Carnegie Mellon University

15-812 (Programming Languages Semantics)

Please refer to "" this link for the most recent schedule updates.

We survey the theory behind the design, description, and implementation of programming languages, and of methods for specifying and verifying program behavior. Both imperative and functional programming languages are covered, as well as ways of integrating these paradigms into more general languages.

Coverage will include:
- program specification and proof (including Hoare logic, weakest preconditions, and separation logic)
- concurrent programming (including shared-variable and message-passing approaches)
- functional programing (including continuations and lazy evaluation)
- type systems (including subtyping, polymorphism, and modularization)

In exploring these topics, we will use a variety of fundamental concepts and techniques, such as compositional semantics, binding structure, domains, transition systems, and inference rules.