On this page, you will find several suggestions for formalization projects in Coq that will serve as an exam for the course.

Note that you can suggest your own formalization project: please contact me by mid january if you plan to do so, soon if you are considering to do so!

The projects are to be handed at the latest by the 16th of february. You should contact me by the 15th of january to let me know which project you intend to present (of course, if you start on your own personal project and ultimately decide to shift on a more guided project, that is still possible, but let me know anyway!)

Here is a list of possible projects, of various difficulty, length and degree of guidance (some are quite/very free, some other projects are quite directed with indications):

• Formalizing Arrow theorem in Coq
• Formalizing regular languages and Brzozowski's derivatives
• Formalizing the cohérence of Heyting's arithmetics
• Study of the power function in Peano's arithmetics
• A certified compiler for a small language
• Formalization of Lebesgue integration
• You can work on other projects if you have you own ideas. One option for instance may be to work on the strong normalization theorems for the simply-typed lambda-calculus and for Gödel's system T from Joly's course of the first semester.