Course Information

CS430/530: Formal Semantics, Fall 2013, Yale University

Last modified: September 5, 2013.


General Information

CS 430/530 teaches the formal semantics of programming languages. That is, a mathematically rigorous description of what a computer program means. The course should be useful to anyone who is serious about programming, and is essential for anyone planning either to do research in programming languages or to design a programming language. The course is intended to accomplish two things: Prerequisites:

You should have taken CS 201 and CS 202 (or equivalents), and have a couple of years of programming experience. CS 223 and CS 323 (or equivalent) are also recommended, but not required.

MW 11:35 AM - 12:50 PM, Room 000 AKW

Zhong Shao, Room 314 Watson, 432-6828, zhong dot shao at yale dot edu
office hours: MW 4 - 5 PM or by appt.

Teaching Assistant:
Shu-Chun Weng, Room 304 Watson, 432-7606. shu-chun dot weng at yale dot edu
office hours: Mon. & Fri. 2 - 4pm, or by appointment (evenings or weekends welcome).


The main required textbooks are:
The following ebook teaches you how to use the Coq proof assistant:

Supplementary Readings

Other supplementary reading materials:


Assignments which require programming can 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 and enroll in cs430 through here.


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


Attendance at lectures is expected but will not be recorded. Students are, however, fully responsible for all material presented in lectures, even if some of it does not appear in the official textbooks. Class attendance is recommended strongly.


There will be approximately 7 assignments, most of which are a set of problems taken from the two textbooks plus possibly some Coq programming. Assignments are due at 11:59 PM on the date specified in the Schedule sheet.

To submit electronic files, including Coq *.v files and any document formats (e.g. pdf, doc) you decide to write your written assignment in, please refer to the section below. Please hand your paper copies to the TA or place them in his mailbox: Watson building room 304.

Each student is given 6 discretionary late days for assignments, but any one assignment may only be up to 3 days late. These are calendar days, not business days. Assignments submitted more than 3 days 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.

How to Submit Programming Assignments

For each programming assignment, you must turn in completed coq *.v files. There must not be any admit or Admitted in the files, or the submission scripts will not accept them (the scripts are not smart enough to detect if they are part of the program or the comments, so avoid them in the comments, too). A coq source file that failed to compile by the /usr/bin/coqc compiler on the Zoo machines is considered NOT submitted; no points will be awarded even for the parts that compile.

To submit your solutions to the programming assignments electronically, you must have an account in the Zoo and be enrolled in cs430. See previous section. First change to the directory where your solutions are, and then use the following command.

     /c/cs430/bin/submit number files
number is the assignment number and files is the list of files for that assignment. For example,
     /c/cs430/bin/submit 2 Induction.v Lists.v Written.pdf
submits the files Induction.v, Lists.v, and Written.pdf for a fictitious assignment 2.

The submit command copies your files to the directory /c/cs430/SUBMIT/number/login and lists all the files that you have submitted for assignment number. Here, login is your user account name.

There is also unsubmit, which allows you to retract one or more files. For example,

     /c/cs430/bin/unsubmit 2 Lists.v
would remove your Lists.v from the submission directory.

You can also check what files you have submitted by using the check command. For example,

     /c/cs430/bin/check 2
would list all the files your have submitted so far for assignment 2.

Keeping In Touch

We will use the piazza forum for announcements and discussions. All the course-related information will be kept at the following site:

Copyright (c) 2013, Zhong Shao, Dept. of Computer Science, Yale University