|
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 abstractly specifying how programs compute (operational semantics), as well as how to describe what programs compute (denotational semantics). Using these specifications, we can proving 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.
| Name | Office | Office hours | ||
|---|---|---|---|---|
| Instructor | Andrew Myers | andru@cs.cornell.edu | Upson 4124 | W 1:30-2:30PM |
| Teaching Assistant | Matthew Fluet | fluet@cs.cornell.edu | Upson 4112 | Th 2-3PM |
| Teaching Assistant | James Cheney | jcheney@cs.cornell.edu | Upson 4142 | M 1-2PM, F 2-3PM |
| Admin. Assistant | Linda Marie Competillo | lmc@cs.cornell.edu | Upson 4107 | M-F 8:30-10AM, 2:30-4PM |
Required text:
Other useful books:
On the programming side, experience with at least a Pascal- 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.
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.
