## CS 611 Course Information |

**Lectures**: MWF 10:10AM to 11:00AM, Olin Hall 218.

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:

*The Formal Semantics of Programming Languages: An Introduction*, Glynn Winskel, MIT Press.

Other useful books:

*Semantics of Programming Languages*, Carl A. Gunter*Foundations for Programming Languages*, John Mitchell*Applied Semantics of Programming Languages*, Franklyn Turbak and David Gifford*A Theory of Objects*, Martín Abadi and Luca Cardelli*ML for the Working Programmer*(*2nd Ed.*), Larry Paulson

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.

- The scribe template and related .sty files for LaTeX are available in
`scribe.zip`. - A TrueType TeX math symbols font for viewing some of the lecture notes
- The Fox project's on-line information about Standard ML.
- The SML/NJ Homepage.
*Programming in Standard ML*, Robert Harper.- The Caml home page.
- Mark Leone's Resources for Programming Language Research
- The inside-the-firewall version of the CS611 web page