Location:
Upson Hall 211
Time: 10:10AM to 11:00AM
Days: Monday, Wednesday, and Friday
Communication with the staff is best done through the
staff mailing list, cs611@cs.cornell.edu.
You are also encouraged to post questions of interest to the whole class on the
newsgroup, cornell.class.cs611. The staff will
generally try to answer questions sent to the
staff mailing list on the newsgroup. Don't expect immediate answers from the
course staff on the newsgroup, especially late at night, over weekends, or
right before the deadline -- use the office hours instead.
| Name | Office | Office hours | ||
|---|---|---|---|---|
| Instructor | Radu Rugina | rugina@cs.cornell.edu | Upson 4141 | Wed 11:00AM-12:00PM |
| TA | Michael Clarkson | clarkson@cs.cornell.edu | Upson 4154 | Tue 4:00PM-5:00PM |
| TA | Sigmund Cherem | siggi@cs.cornell.edu | Upson 5152 | Thu 1:30PM-2:30PM |
| TA | Brian Hackett | bwh6@cornell.edu |
The goal of this course is to study formal techniques for describing
computation and compilation. This approach leads to a more general
understanding of programming languages, specification, logic,
mathematics, and proof theory, and provides a framework for precisely
characterizing a variety of programming languages.
We will study how to formally specify how programs execute
(operational semantics), how to describe what mathematical functions
programs compute (denotational semantics), and how to use logic to
characterize properties and invariants of the program execution
(axiomatic semantics). Using these specifications, we can prove
interesting and relevant properties of programming languages: for
example, that a programming language has a sound type system, or that
a compiler preserves type safety. These techniques have significant
practical utility and are becoming increasingly relevant to other
areas of computer science.
On the programming side, experience with at least a Pascal, Java, or C-like language is assumed. Preferably, students will
have some knowledge and experience working with a functional language, such as Scheme, ML, or Haskell. The
more experience with programming in different programming languages, the better.
On the theoretical side, we assume a basic proficiency in undergraduate mathematics, logic, and computer science.
A basic knowledge of computability (such as Turing machines and recursive functions) and logic (that is, predicate
calculus), as well as some mathematical maturity is required.
This course is designed for PhD or MEng students in CS, Math, OR, and EE. If you are an undergraduate student,
you must talk to the instructor to find out if the course is suitable for you. MEng students are also recommended to
speak with the instructor in cases of doubt.
Required text:
1) The Formal Semantics of Programming Languages: An Introduction, by Glynn
Winskel
Useful texts:
2) Semantics of Programming Languages, by Carl Gunter
3) Foundations for Programming Languages, by John Mitchell
4) Types and Programming Languages, by Benjamin Pierce
5) Principles of Program Analysis, by Fleming Nielson, Hanne Riis Nielson,
and Chris Hankin
Copies of these books will be on reserve in the Engineering library.
Grades will be assigned in CS 611 on the basis on several factors. There are six homeworks, which collectively are worth 40% of your grade. The preliminary exam is worth 20%, and the final exam is worth 30%. You will also be asked to scribe about 2-3 lectures (depending on the number of students in the class); the final 10% of your grade is based on this and other class participation. These percentages are intended only as guidelines; they may be adjusted as the course progresses.
Homework and programming assignments will be accepted after the deadline, but at a penalty. When assignments are turned in late, the penalty increases linearly by 10% each day: 10% for one day late, 20% for two days late, 30% for 3 days late, etc. (so don't turn them in later than 10 days past the due date).
Cornell University has a Code of Academic Integrity, with which you should be familiar. Violations of this code are treated very seriously by Cornell and can have long-term repercussions. In this course, you are encouraged to discuss the content of the course with other students, and you may also discuss homework problems with other students. However, you must do your own work, and if you discuss a problem with another student, you are expected to document this fact in your write-up. It is a violation of the code to copy work, including programs, from other students; it is also a violation to use solutions to homework problems from previous iterations of the same course. Note that Cornell holds responsible for the code violation both the recipient and the donor of improper information.