Lectures will be held Monday, Wednesday, and Friday, from 10:10AM to 11:00AM, in Olin Hall 218. Communication with the staff is best done through the staff mailing list, cs611@cs.cornell.edu. You may also post questions of interest to the whole class on the newsgroup, cornell.class.cs611. When appropriate, the staff may also answer questions sent to the staff mailing list on the newsgroup.
| Name | Office | Office hours | ||
|---|---|---|---|---|
| Instructor | Radu Rugina | rugina@cs.cornell.edu | Upson 4141 | Wed 11:00AM-12:00PM |
| Teaching Assistant | Stephen Chong | schong@cs.cornell.edu | Upson 5157 | Thu 2:30-3:30PM |
| Admin. Assistant | Juanita Heyerman | juanita@cs.cornell.edu | Upson 4147 |
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:
The Formal Semantics of Programming Languages: An Introduction by Glynn
Winskel
Useful texts:
Semantics of Programming Languages by Carl Gunter
Foundations for Programming Languages by John Mitchell
Types and Programming Languages by Benjamin Pierce
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 up to 4 days late, 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.