CS 430/530, Spring 2002. Course Information

CS 430/530 Course Information


General Information

Lectures:
MWF 11:30 AM -12:20 PM, Room 400 AKW

Instructor:
Zhong Shao, 314 Watson, 432-6828, shao-zhong@cs.yale.edu,
office hours: MWF 12:20-1:00 or by appt.

Teaching Assistant:
Nadeem A. Hamid, 305 Watson, 432-1274, nadeem@acm.org,
office hours: TBA or by appt.


Textbooks and Supplementary Readings

The main required textbooks are:
  • John Reynolds. Theories of Programming Languages. Cambridge University Press, 1998. ISBN 0-521-59414-6. Buy it online or get it from the Yale bookstore.
  • Robert Harper, Programming Languages: Theory and Practice. School of Computer Science, Carnegie Mellon University, November 2001. Working draft available for downloading: 2up PS or 2up PDF. You can also get it from the author's website (which also includes an online PDF file). .
  • The following book is strongly recommended (especially to those who have not had much training in formal logic). We'll only cover (parts of) Chapters 1-2 in class, but the rest of the book is also well-written and interesting.
  • Michael Huth and Mark Ryan. Logic in Computer Science: Modelling and reasoning about systems, Cambridge University Press, 2000. ISBN 0-521-65602-8. Buy it online or get it from the Yale bookstore.
  • We may also cover selected parts of the following papers and documents (this list is not quite up-to-date yet):
  • Henk Barendregt. Lambda Calculi with Types. Download the reprint. Also in Handbook of Logic in Computer Science (Volume 2), Oxford University Press, 1992.
  • Henk Barendregt and Herman Geuvers. Proof-Assistants Using Dependent Type Systems. Download the reprint. Also in Handbook of Automated Reasoning (Volume 2), MIT Press, 2001.
  • C. A. R. Hoare. An Axiomatic basis for computer programming. Comm. ACM. 12(10), pages 576-580, 583 (1969). Available here (PDF) in the ACM digital library.
  • C. A. R. Hoare. Assertions: a personal perspective. June 2001. Available here in Hoare's web page.
  • C. A. R. Hoare. Software: barrier or frontier. Nov 1999. Available here (PDF) in Hoare's web page.
  • George Necula. Proof-carrying code. In POPL'97. Available here in Necula's web page.
  • Philip Wadler. Proofs are Programs: 19th Century Logic and 21st Century Computing. June 2000, updated November 2000. Download the article. There is also a less technical version published in Dr. Dobb's Special Report, December 2000.
  • Other supplementary reading materials:
  • J. D. Ullman, Elements of ML Programming (ML97 Edition), Prentice-Hall 1998.
  • S. Thompson, Type Theory and Functional Programming, Addison Wesley 1991. ISBN 0-201-41667-0.
  • Glynn Winskel, The Formal Semantics of Programming Languages, The MIT Press, 1993. ISBN 0-262-23169-7.
  • M. J. C. Gordon, The Denotational Description of Programming Languages, Springer-Verlag 1979. ISBN 0-387-90433-6.
  • R. Tennent, Semantics of Programming Languages, Prentice Hall 1991. ISBN 0-13-805599-8.
  • R. Milner, M. Tofte, B. Harper, D. MacQueen. The Definition of Standard ML (revised), The MIT Press, 1997. ISBN 0-262-63181-4.

  • Computers

    Occasional programming assignments will be done using the Linux PCs in the Zoo. If you plan to take the course for credit, you should have an account on these machines.


    Grading

    Your grade will be calculated as follows: These weights are subject to minor variation.


    Attendance

    Class attendance is recommended strongly.


    Assignments

    Each student is given 100 discretionary late hours for problem sets and programming assignments, but any one assignment may only be up to 72 hours late. These are calendar hours, not business hours.

    After you use up all of your discretionary late hours, assignments turned in late will be graded according to the following formula: S = R * (1 - t / c), where S is the grade given, R is the grade the work would have gotten if turned in on time, t is the amount of time by which the work was late, and c is equal to four days. Thus, the value of a late assignment decays daily, with a half-life of just over two days. Examples: work turned in five minutes late gets 99.9% credit, one hour late gets 99.0% credit, six hours late gets 93.8% credit, one day late gets 75.0% credit, two days late gets 50.0%, and three days late gets 25.0%. Assignments submitted more than 72 hours late will not be accepted.

    There will be no extensions due to scheduling conflicts, computer downtime, or other such factors, except under truly extraordinary circumstances. Extensions will be granted only for university-sanctioned excuses such as illness, and then only with the proper documentation. You are responsible for planning ahead and managing your time so that you can complete the assignments on time. You must either finish on time or accept the consequences of doing otherwise.


    Keeping In Touch

    The best way to contact the instructor and the TA is by electronic mail. To get help quickly, your best bet is to send email to cs430@cs.

    All the course-related information will be kept at the following web site:

              http://flint.cs.yale.edu/shao/cs430/index.html
    

    Also, yale.cs.cs430 is a local newsgroup specifically for CS 430/530. You should read both the course home page and the newsgroup rather frequently as they appear for important information, such as lecture notes, instructions on submitting your assignments, clarifications and hints, last minute schedule changes, etc.


    Copyright (c) 1996--2002, Zhong Shao, Dept. of Computer Science, Yale University