General Instructions

The final project in CS 263 contains two parts:

• an assignment like normal ones (but longer), done alone (15pt);
• an open-ended programming language theorem proving project, done in a small team (35pt).

The rest of this page explains what you are expected to do in the second part. You should strongly consider using a version control system (e.g., git or svn) to manage the files for the source code in this project.

Topics

The open-ended project should be a Coq theorem proving project. Its topic should be related to the programming language theory or program verification. Here is a list of possible topics (a detailed explanation can be found here http://jhc.sjtu.edu.cn/public/courses/CS263/Topic_List.html):

• Bourbaki-Witt fixpoint theorem
• Equivalence among 3 denotational semantics
• Equivalence among 7 definitions of reflexive transitive closure
• Hoare logic's completeness theorem
• First order logic's soundness theorem
• First order logic's completeness theorem
• Algorithm Correctness of Mobius transformation
• Algorithm Correctness of discrete Fourier transform
• Algorithm correctness for calculating longest increasing subsequence
• Implementation Correctness of binary search tree's via VST
• Semantic equivalence for programs with break and continue
• Semantic equivalence for programs with run-time error and nondeterminism

Students CAN pick a project which is NOT on this list above. Students can even pick a project that overlaps with their lab work. For example, students who do research in a network lab may be interested in formalizing and verifying a network protocol. But keep in mind that CS 263 final projects must be self-contained. We will discuss other ideas during the class or by email. At most 3 teams may choose the same topic. For a popular topic, which teams may work on it is determined by a first-come-first-get basis. So, send your proposal as early as possible!

Teams

Each team can contain 3 or 4 students. A team may have 1, 2 or 5 students with permission of the instructor, although it is not suggested. Teams with more than 5 members are not allowed.

Schedule and Check Points

Team member confirmation

Due date: May 9. All team members should send emails to TA, Shuyang Tang, listing the members' name of your team. Every team should have a team leader. His or her name should be highlighted in the email.

Proposal submission

Due date: May 21. Every team leader should send an email to the instructor describing what you want to prove in English or Chinese.

Midterm report

Due date: June 4. Every team leader should send your latest version (one or more Coq files) to the instructor via email. It should at least contain necessary definitions and your theorem's statement.

Final submission

Due date: June 24. Every team leader should send your final version to the instructor by email. It should contain all your Coq development and a README file explain the order of compilation and the main proof steps in english (very short).

Grades

Your final project's grade is composed by the following three parts: Part 1: 20 points for task completion (graded after submission):

• 20 : complete;
• 16 - 19: small number of minor holes appearing in proofs;
• 12 - 15: big number of minor holes appearing in proofs;
• 8 - 11 : one major hole in proofs;
• 0 - 7 : more than one major holes in proofs.

Part 2: 5 points for being elegant in proofs (graded after submission). Part 3: 10 points for task's difficulty (graded when tasks are settled after midterm report). In principle, all members in the same team will get the same grade.