15-812A Programming Language Semantics

15-812A Programming Language Semantics (12 units) Spring 2010

John C. Reynolds

University Units: 12 (starred course)

Tuesdays and Thursdays, noon-1:20 pm, GHC 4303

Course Description

We survey the theory behind the design, description, and implementation of programming languages, and of methods for specifying and verifying program behavior. Both imperative and functional programming languages are covered, as well as ways of integrating these paradigms into more general languages. Coverage will include:

In exploring these topics, we will use a variety of fundamental concepts and techniques, such as compositional semantics, binding structure, domains, transition systems, and inference rules.

PREREQUISITES: There are no specific prerequisites, but the course requires some background in programming languages and basic mathematics. To get a feel for what is needed look at Appendix A of the text and skim over the first couple of chapters. If these seem unduely difficult, meet with the instructor.

TEXTBOOK: J. C. Reynolds, "Theories of Programming Languages", Cambridge University Press 1998 (hardback), 2009 (paperback) (The contents of the hardback and paperback are identical.) (errata in postscript) (errata in PDF)

RESERVED BOOK LIST (postscript) (PDF)

ADDITIONAL READING: Each chapter of the textbook gives bibliographic notes listing journal articles and reserved books. This material is not required reading; it is there in case you have difficulty in understanding the text or want to pursue a topic further for your own interest.

HOMEWORK: There will be homework assignments, at most once a week. No late homework will be accepted. However, the two lowest grades will be dropped before averaging the grades. Collaboration is permitted on homework, but each person must write up his own answers and must be able to demonstrate that he understands them.

EXAMINATIONS: There will be midterm and final examinations. Both will be open-book exams. No collaboration is permitted.

GRADING: Your grade will be computed in two ways: as an equally weighted average of the homework, the midterm, and the final, and as an equally weighted average of just the midterm and the final. Your actual course grade will be the higher of the two.

COVERAGE: The goal is to teach as much as can be taught clearly, not to cover all of a fixed syllabus. You will not be examined on topics that are not covered in class, unless it is specifically announced otherwise.

ASKING QUESTIONS: It is vital that you ask questions if an explanation seems unclear. There may also be bugs in the textbook: If you find one you should bring it up in class if it is likely to mislead anyone, or report it to the instructor privately if it is minor.

ADDRESSES AND OFFICE HOURS
Instructor: John Reynolds, GHC 9019, #8-3057 john.reynolds AT cs DOT cmu DOT edu

Secretary: Tracy Farbacher, GHC 9129, #8-8824, tracyf AT cs DOT cmu DOT edu

Copies of handouts will usually be available outside this office.

CLASS WEBPAGE: /www.cs.cmu.edu/afs/cs.cmu.edu/project/fox-19/member/jcr/www15812As2010/cs812-10.html
There is a link to this page from the instructor's home page at /www.cs.cmu.edu/~jcr.
Check this page frequently - important or unexpected notices will be posted prominently.

NOTICE: The first class will be January 12; the last class will be April 29.

NOTICE: There will be no class on March 9, March 11, or April 15.

Last updated: January 11, 2010