Since the official timing of the final examination for the course is “Monday : April 22 Afternoon” according to the SCC’s timetable, I will tag the final submission at 5:00 pm on Monday, April 22. 2019. For questions, clarifications and comments, please comment at the corresponding issue.

Goals

The goals of the project are to illustrate the integration of computation and proof in Dependent Type Theory.

Rules and Criteria

• The code must output a solution together with a proof that it is correct.
  • It should be transparent from the output type that it proves the correct result, i.e. the evidence should not be c a complicated type that is not clearly correct.
  • if complex types help for internal computation it is a good idea to introduce them, but they should be translated to simpler ones for both input and output.
• Only valid input should be accepted, i.e., evidence for any conditions that need to be satisfied should be arguments.
  • if the evidence is hard to supply, also write helpers making it easy to generate such evidence. For example, if you need that an input is prime, there should be a complementary function to easily prove 7 is a prime.
• Credit is given both for useful algorithms and non-trivial proofs of correctness.
• Document the code.
• Give examples, typically in different files.
• Proof should be usable as arguments to other functions, e.g. a proof that a number is even should be usable in conjunction with a function requiring an even number.
  • the best projects will in fact have a tree where several pieces of evidence that are results of functions are used by other functions that need these as conditions.

Final Submission guidelines.

• By the final submission, I expect complete code
  • no missing definitions
  • functions total, with the only exception for components of an interpreter (as interpreters cannot be total).
  • achieving the guidelines, i.e. accepting only valid input and giving output including proofs that the output satisfies all claimed properties.
• Only pull requests that pass the tests are merged.
• Please update reports along the same lines as the midterm submission.