General Instructions

The final project in CS 263 (excluding isolated quizes) is an open-ended programming language theorem proving project, done in a small team (25pt). The rest of this page explains what you are expected to do in this project. 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 will be attached):

• Bourbaki-Witt fixpoint theorem and its three applications
• Knaster-Tarski fixpoint theorem and one of its application
• Equivalence among 3 denotational semantics and small step semantics
• Small-steps vs. denotations for programs with break and continue
• Denotations vs. Hoare logic for programs with break and continue
• Small-steps vs. denotations for programs with function calls
• Equivalence among denotations for programs with function calls
• Denotations vs. Hoare logic for programs with function calls
• Executable semantics for lambda calculus with reference and IO
• Executable semantics for programs with addresses, fork/join and IO
• Denotation-based transformation correctness for constant folding
• Simulation-based transformation correctness for constant folding
• Simulation-based transformation correctness for dead assignment elimination
• Denotation-based transformation correctness for dead assignment elimination
• Algorithm correctness of Strassen's matrix multiplication
• Algorithm correctness of Mobius transformation
• Algorithm correctness of discrete Fourier transform
• Algorithm correctness of splay operation
• Implementation correctness of doubly linked list via VST
• Implementation correctness of splay operation via VST
• Implementation correctness of threaded BST via VST
• Implementation correctness of red-black tree insertion via VST

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 in class, in course QQ group or by email. Two teams cannot choose the same topic. For a popular topic, which team 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 2 or 3 students. A team may have 1 or 4 students with permission of the instructor, although it is not suggested. Teams with more than 4 members are not allowed.

Schedule and Check Points

Team member confirmation

Due date: May 1. All team members should send emails to intructors, 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 7. Every team leader should send an email to the instructor describing what you want to prove in English or Chinese.

Midterm report

Due date: May 25. 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, your theorem's statement and important intermediate results' statements.

Midterm report - second check

Due date: June 4. If impractical designs appear in your midterm submission, instructors will email you and discuss related details. You should fix these problems by June 4.

Final submission

Due date: June 25. 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 two parts: Part 1: 20 points for task completion:

• 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;
• one or two points may be taken off if you miss check points;
• one or two points may be taken off if important defitions and intermediate results are not clearly stated.

Part 2: 5 points for task's difficulty:

• 1: 4-student team on normal projects
• 3: 3-student team on normal projects
• 4: single student or 2-student team on normal projects
• 5: self designed hard projects (graded when tasks are settled).

In principle, all members in the same team will get the same grade.

Why you should use a version control system

We highly recommend you to use a version control system (e.g., git or svn) to manage the files for the source code in this project. Here is why.

• Popular version control systems are very accesible.
• Most IT companies use version control systems. You need to get familiar with it anyway in the future.
• You will not lose your developement (maybe 2 or 3 weeks work) due to a computer breakdown.
• You may have some back-and-forth when desiging definitions and proofs. Version control systems can help you find your earlier versions back.
• A version control system help record the contribution of every individual. If your teammates complaint that you does not work hard on the project, you can use these record to justify your own contribution.