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

John C. Reynolds

University Units: 12 (starred course)

Mondays and Wednesdays, 1:30-2:50 pm Wean Hall 7220 (NOTE CHANGE)

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. (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, Wean 8126, #8-3057 john.reynolds AT cs DOT cmu DOT edu


Secretary: Margaret Weigand, Wean 8110, #8-2568 weigand AT cs DOT cmu DOT edu

CLASS WEBPAGE: /www.cs.cmu.edu/afs/cs.cmu.edu/project/fox-19/member/jcr/www15812As2008/cs812-08.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: There will be no classes on January 21 (Martin Luther King Day), February 4 or 6.

NOTICE: Exercises 1.4 (parts a and b), 1.5, and 2.2 in the text were assigned as homework on January 28. They were due on February 11, and returned with grades on February 20.

NOTICE: Exercises 3.3(b) and 3.6 in the text were assigned as homework on February 11. They were due on February 20. The answer sheets are available from the holder on the door of Wean Hall 8110.

NOTICE: Exercises 5.3 and 5.4 in the text were assigned as homework on February 20. They will be due on February 27.

NOTICE: Exercises 6.2 (parts b and c) and 7.4 in the text were assigned as homework on February 27. They will be due on March 5.

NOTICE: The midterm exam is an open-book take-home exam that was given out on March 17 and will be due on March 24. It covers material taught in class up to and including the class on March 3.

NOTICE: The median grade on the midterm was 81.

NOTICE: Exercises 10.1 (first expression only), 11.7, and 11.9 in the text were assigned as homework on March 31. They will be due on April 7.

NOTICE: Regarding Exercise 10.1(d), on page 206 of the text: "... a closed expression e is said to evaluate eagerly to a canonical form z, written e =>_E z, if there is a reduction sequence from e to z in which each contraction acts on the leftmost beta_E-redex that is not a subexpression of a canonical form."

NOTICE: Exercises 12.1, 12.4, and 13.2 in the text were assigned as homework on April 14. They will be due on April 21.

NOTICE: A number of students turned in unusual, though incorrect solutions to Exercise 11.9. I will discuss the difficulties with these solutions in class on April 21.

NOTICE: Exercises 14.3c, 14.3d, and 14.5 in the text were assigned as homework on April 23. They will be due on April 30.

NOTICE: The final exam is an open-book take-home exam that was given out on April 30 and will be due on May 7.

NOTICE: ON THE FINAL EXAM: (1) On the last line of the display in Question 3, the subscript "eq" should be "ref". (2) On the first line of the display in Question 5(d), a closing parenthesis should be added at the end of the line

Last updated: May 1, 2008