Guidelines for projects

[siddhartha-gadgil]

This is posted as an issue since questions and discussion are welcome.

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.

[Chinmaya-Kausik]

What exactly comes under useful algorithms, per se?

Considering that we have some projects where the only non-proof elements are definitions of structures and recursive definitions of operations, sometimes suitable definitions also requiring foresight into proofs, could you clarify which of these, if any, will receive credit?

As in, are recursively defined operations (e.g. addition or multiplication in certain structures) considered useful algorithms? And do important definitions count, or are they considered too less of a contribution?

[siddhartha-gadgil]

Useful algorithm means that the result is useful. This includes, for example the quotient group with its universal property, since one does often want to pass to the quotient. Here most of the work is defining basic operations.

Is there a specific example different in nature from the above that you are unsure about?

[siddhartha-gadgil]

Just wanted to say that a lot of the work done so far is really impressive.

[siddhartha-gadgil]

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.

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.