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. The timeline for meeting and proposal are given below:
Proposal Due: Nov 12
Project Due: (write up due): December 9
We are open to any proposal that arguably deepens the student’s knowledge. If you can think of a way to tie this project to your actual research (e.g. by formalizing some aspect of your work), that could also work. Depending on the scope of the project, projects with 2-3 students are also allowed.
Here are some ideas for projects:
Verification project.There are many medium-sized well-known algorithms that would be interesting to formalize and prove correct. Examples that should give you a broad idea of the scope include (but are not limited to):
Sorting algorithms (1 person). You can take a look at the Verified Functional Algorithms volume of software foundations that covers correctness of insertion and selection sort. Any other algorithm (e.g. bubblesort/quicksort/mergesort) would be a good candidate. All three can be quite tricky though!
IMP on steroids (2 people). Extend IMP with an array like construct (+ Hoare Triples to reason about them). Implement some interesting algorithm on top and verify its correctness (e.g. the sorting algorithm from the previous bullet).
System F (1 person). System F is an extension of the STLC with polymorpshism. Implement System F and prove progress and preservation.
You can use QuickChick to systematically inject bugs into developments and ensure that your test generators find them. You could also extend the verification projects above to include an additional testing component by adding one person.
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. 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.
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.
Explore other proof assistants.
Pick another proof assistant of your choice (a good list is available in the project page for the spring offering of this course. Choose a formalization we’ve done in Coq and repeat it in the other proof assistant.