The course has three broad topics:
The first part of this graduate-level course focuses on the semantics of a variety of programming language constructs (e.g., "what does a while loop really mean?" -- this is actually much more exciting than it sounds). We will study structural operational semantics as a way to formalize the intended execution and implementation of languages. Operational semantics concepts and notation are widely used in modern PL research. We will survey axiomatic semantics, which is useful in developing as well as verifying programs. Axiomatic semantics underpin recent research efforts in formal verification and bug finding (e.g., proof-carrying code and SLAM). We will pay a brief lip service to denotational semantics, whose deep mathematical underpinnings give it exceptional versatility and rigor, but, alas, also mortis. We will apply these techniques to imperative, functional and object-oriented languages. We will follow the presentation of these topics in Glynn Winskel's The Formal Semantics of Programming Languages.
The second part of this course covers the techniques used in the study of type systems for programming languages. We will start our study with the simply typed lambda calculus and continue with more advanced features such as types for imperative features and exceptions, parametric polymorphism, existential types for use in abstraction and module systems, and dependent types. Type systems abound in modern PL research and make up the vast majority of the "Greek letters" found in current papers. Understanding and presenting new type systems is of critical importance when doing work in this area. A good additional reference for this part of the course is John Mitchell's Foundations for Programming Languages.
The last part of the course covers special topics, possibly presented by expert invited speakers, drawn from recent research in topics like: the semantics of object-oriented languages; region-based memory management; type systems for resource management; software model checking; counter-example guided abstraction refinement; and automated theorem proving and proof checking. The list of lecture topics also serves as summary of key course concepts.
In addition to the topics studies in class, students will have the opportunity to consider other related topics of interest in the form of a course project, most often in the form of a survey of recent research on a topic of interest.
An assignment turned in d days late has its point value reduced by (d * 10)%. We follow the Honor System.
