During my final year at university, I did a project on learning to use Coq and rewriting some proofs from the Coq standard library. I produced a report and did a presentation. See the links below for the files.
