Other supplementary reading materials:
- Adam Chlipala.
Certified Programming with Dependent Types, 2013.
- Michael Huth and Mark Ryan.
Logic in Computer Science: Modelling and Reasoning about Systems (2nd Edition; Paperback).
Cambridge University Press, 2004. ISBN 052154310X.
- Hanne Riis Nielson and Flemming Nielson.
Semantics with Applications: An Appetizer. Springer, 2007. ISBN 1846286926.
- Benjamin Pierce.
Types and Programming Languages.
The MIT Press, 2002. ISBN 0262162091.
- Henk Barendregt and Herman Geuvers.
Proof-Assistants Using Dependent Type Systems.
In Handbook of Automated Reasoning (Volume 2),
MIT Press, 2001. The Postscript version is available
online in Herman Geuvers'
publication page
(under year 2001).
- Yves Bertot and Pierre Casteran.
Interactive Theorem Proving and Program Development.
Springer, 2004. ISBN 3540208542.
- Glynn Winskel. The Formal Semantics of Programming Languages. The MIT Press, 1993. ISBN 0262231697.
- John Mitchell. Foundations of Programming Languages. The MIT Press, 1996. ISBN 0262133210.
- R. Tennent. Semantics of Programming Languages.
Prentice Hall 1991. ISBN 0138055998.
- Henk Barendregt. Lambda Calculi with Types.
In Handbook of Logic in Computer Science (Volume 2),
Oxford University Press, 1992.
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:
- class participation: 10%
- problem sets and/or programming assignments: 60%
- final project and/or exam: 30%
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.
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.
We will use the Ed Discussion forum for announcements and discussions.
See the Quick Start Guide to learn how to use Ed Discussion.
Copyright (c) 2025,
Zhong Shao,
Dept. of
Computer Science,
Yale University
