Main | Lectures | Homework | Projects | Piazza Forum

CS 6610 - Design And Analysis Of Programming Languages

Lectures and Details

Is This A Good Course?

Shopping around? My webpage has previous teaching evaluations.

Course Overview

This course is designed to acquaint you with the fundamental ideas behind modern programming language design and analysis. Ultimately you should be able to understand current research and apply the techniques here to your own projects.

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 also cover satisfiability modulo theories, automated theorem proving, DPLL(T), and proof checking. 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.

Course Prerequisites

The prerequisites for this course are programming and mathematical experience. The ideal programming experience is an undergraduate compilers course as well as practical exposure to several different programming languages, such as C, ML, LISP and Java. The ideal mathematical experience is a knowledge of mathematical logic and the ability to construct rigorous proofs (in particular by structural induction). These prerequisites are not strict. However, your desire to be exposed to this material is very important. In the past a small number of undergraduates have been able to complete the course.

Assignment Overview

You will be responsible for: The relative weighting is such that you could skip all of the homeworks and do a bang-up job on the project and still get an A.

An assignment turned in d days late has its point value reduced by (d * 10)%. We follow the Honor System.

Alternate Grading Contract

In response to student demand, you have the option (this is not required) of committing to the following grading contract: This grading contract may be appropriate for students pursuing a self-funded coursework-based professional Master's degree, for example. Such students may not be interested in pursuing a research career and may not have the time to give full attention to all aspects of this course.

Note the following degree requirements, reproduced from the Graduate Handbook:

To opt-in to this alternate grading contract, simply send me email.


Your class work might be used for research purposes. For example, we may use anonymized student assignments to design algorithms or build tools to help programmers. Any student who wishes to opt out can contact the instructor to do so after final grades have been issued. This has no impact on your grade in any manner.

Students interested in considering graduate or undergraduate research should make an appointment to talk about it. I am happy to discuss graduate matching, independent study projects, SEAS STS senior theses, CLAS Distinguished Major theses, paid research work over the summer, research work for credit, and graduate school applications.

Optional References

You may find the following additional resources helpful: Finally, I give mock orals (and associated study tips) to students preparing for the Quals. If time is limited I favor the students in my class.