COMP 293: Course Project and Presentation — Implementation
In this course project, you will implement and verify your algorithm of choice in Coq proof assistant,
and summarize the results in a final presentation.
There will be four deliverables:
Submission Description Point Value
Proposal Informal description of algorithm and correctness properties 10%
Implementation Implementation of the algorithm in Coq 30%
Verification Studying correctness results in Coq 40%
Presentation Summary of results presented to class 20%
1 Implementation
In this phase, you are implementing your proposed algorithm in Coq proof assistant. A Coq implementation
of the algorithm may accompany the definition of all required data types, e.g., lists, trees, graphs, etc.
For each function that you define, provide a number of unit tests that explore different potential scenar-
ios. This helps you get a better idea of how your code behaves, before getting into the detailed proofs of
correctness in the next phase.
2 Deliverables
You will submit all your Coq source files in Canvas, as a single package. Please provide a short READ ME
file specifying the structure of the files and their dependencies.
1



















学霸联盟