Lectures | Homework | Projects

CS 655 - Design And Analysis Of Programming Languages

Lectures and Details

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 the semantics of object-oriented languages, abstract interpretation and applications of program semantics in program analysis and verification. This part of the course may also cover several novel applications of ideas from language semantics to system security in the presence of untrusted code, such as proof-carrying code, typed assembly language, Java bytecode verification and typing and type systems for securing the flow of information.

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