5 Project
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.
Some candidate project ideas are listed here - discuss with the instructor if any of them pique your interest!
IMP + IFC, prove noninterference
Targeted Property-Based Testing for QuickChick
QuickChick for F*
Combinatorial Testing for QuickChick
Using QuickChick to test OCaml programs with Coq-of-OCaml
However, several categories of projects would be acceptable:
Reproduction or mechanization. Many program analysis tools or languages are available; a good project might involve running the tool on a benchmark suite in an attempt to reproduce a result given in a paper. The benchmark suite could be varied, or the tool could be compared against a different baseline, in an attempt to (in)validate general claims made in a paper.
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.
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.
Project Presentations
Prepare a 5 minute per person (hard limit of 10’) presentation of what you’ve done.
Can be in the form of slides, a demo, or a combination of the two. Don’t just show your code!
If you want to show code, select one or two interesting bits: the main theorem you proved, the cool QuickChick property you wrote, some particularly crazy bit of Coq/Ltac. But don’t just do a code tour!
Give a high level description of what your goal was when you started.
Give a high level description of where you are currently in the project.
Add anything that might be interesting/worth sharing: Something you learned/something you’d do different/something that Coq did weirdly/etc.