|
The goal of this course is to study formal techniques for describing computation so that properties of programs and programming languages can be analyzed and proved. 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.
For example, we will study how to abstractly specifying how programs compute (operational semantics), as well as how to describe what programs compute (denotational semantics). The abstract but precise realization of these notations allows us to study techniques for formally proving interesting and relevant properties of programming languages: for example, that a program is type-safe, or that a compiler translates programs correctly. These techniques are finding great 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-2 |
| Teaching Assistant | Steve Zdancewic | zdance@cs.cornell.edu | Upson 4104 | F 11-12 |
| Admin. Assistant | Linda Marie Competillo | lmc@cs.cornell.edu | Upson 4115 |
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.
CS 611:
Semantics of Programming Languages