Lectures | Homework | Projects

CS 615 - Design And Analysis Of Programming Languages

Lectures and Details

Is This A Good Course?

Shopping around? The course evaluations from last semester are available (some of my students signed their names in the freeform comments, so those are elided). In addition, unedited testimonials from previous students are available.

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 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.

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.

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.