Main |
Lectures |
Homework |
Projects
| Piazza Forum
CS 6610 - Design And Analysis Of Programming Languages
Lectures and Details
- Meetings: Monday and Wednesday, 2:00pm to 3:15pm in
Rice Hall 340.
- Instructor: Wes Weimer.
- Office Hours: Thursday 11am-Noon or by
appointment (just send email). 423 Rice Hall.
- Teaching Assistant: None.
- However, many students who taken the class previously have access to
the Piazza Forum and are willing to help out.
- Textbook: Glynn Winskel's The
Formal Semantics of Programming Languages.
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:
- Semantics
- Type Systems
- Research Applications
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:
- Homework assignments. There will be
around six "mathematical" or "formal" problem sets for you to complete by
yourself. The homework assignments mostly occur at the beginning of the
course. The final assignment has a non-trivial implementation component and
involves applying an analysis to real code. After that your time is spent
on ...
- A Final Project. You will create a
final project that explores, extends or experiments with the ideas in the
course.
- Reading. While this is not, strictly speaking, a seminar
course, there will be a required paper or book chapter assigned after every
lecture. Reading quizzes may be employed.
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:
- You do not complete any of the Homework Assignments.
- You do participate in class.
- You do complete the Final Project.
- Your final grade is one letter grade lower than it would be
otherwise. That is, if your Final Project and participation would
otherwise merit a grade of "A", you would receive a grade of "B" (because
you did not complete the homework assignments).
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:
- No grade lower than a "C" will be accepted toward satisfying the
Master's degree credit requirements.
- The average of all grades in courses used to satisfy CS graduate
degree requirements must be at least a "B".
To opt-in to this alternate grading contract, simply send me email.
Research
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.