5 Project
Final project proposals are due on Nov. 10. The final project itself will be due on the “reading day” Dec. 14, just after the last day of class, with late submissions accepted until Dec. 21 at a 10% penalty.
Students will more deeply explore a relevant topic of their interest as part of project undertaken the latter portion of the class. Students should meet with the instructor to agree on the basic direction of their project, and ultimately produce a 1-page plan to be approved by the instructor.
We are open to any proposal that arguably deepens the student’s knowledge. Depending on the scope of the project, projects with 2-3 students are also allowed. Here are several categories of project that would acceptable:
Survey. Pick an area of automated reasoning that you are interested in, and do a survey of 10 papers in that area. This is a single-person project.
Mechanization – Reproduction. Type systems, program analyses, and other ideas are often formalized in research papers using mathematical notation. A good project would be to mechanize such a formalization in Coq and with it prove relevant theorems. In essence, this is "reproducing" a result with greater confidence. Older, simpler papers might be good targets here. Instructors will have suggestions. On a related note: Students could also propose to formalize a system that was previously described only informally and potentially (dis)prove unverified claims about it. Proposal should include the paper and proposed task (e.g., just mechanize type safety, not other stuff). Can be 1-3 people, depending on the scope.
Mechanization - Extension. Pick an open-source Coq mechanization and extend it in some way, ultimately submitting that extension as a PR. The proposal should include the target mechanization and the proposed extension, with an estimation of work needed. The extension can be something already proposed, or something you invent. Can be 1-3 people, again, depending on the scope.
Mechanization - Testing. Pick an open-source Coq mechanization and develop QuickChick-based property testing for it. Use this testing framework to show that a proved-correct theorem, when a bug is added, can be discovered by the tester. The proposal should include the target mechanization and the proposed extension, with an estimation of work needed. Can be 1-2 people.
Mechanization - Verify CMSC430 Compiler. For those students who have taken 430: Take the 430 compiler and build a verified version of it. There’s an idealized assembly language called a86. You could write an interpreter for it. There is an interpreter for the source language. Prove that compilation preserves the meaning of programs. What’s nice about this is the compiler is written as a progression of larger and larger subsets of the final language, so you could start by verifying the compiler for a very simple language then grow the mechanization and see how far you get. DVH said he’d be happy to help.
Research project. Students are also free to propose a research project, which aims to develop and evaluate a new idea. Doing this might involve a formalization, implementation/extension, or both. Given the short timeline, such projects will likely involve multiple students. We are open to having projects joint with another class.
Other ideas welcome! In the best case, float the basic concept to the instructor before the 10th.