Le Teaser (work in progress)

Pierre Castéran

About this project


The main objective of this document is to share the pleasure we have had to write developments in Coq for several years.

We plan to respect the following structure :

Participation is welcome

Any form of participation is welcome: correction of errors, improvement of Coq scripts, proposition of inclusion of full chapters, any generally any comment or proposition that would help us.

Current state

In order to get the largest possible feedback from the community, we decided to make available even the first drafts of the ongoing document.
At present, the text is being written and is very incomplete, and we are adapting some proofs written for older versions of Coq, in order to incorporate quite new features, such as type classes, setoid rewriting etc.
Thus, there remains a lot of old-fashioned Coq and still Admitted results. We're working hard for improving this situation, but any help will be acknowledged.


Email : pierre dot casteran at labri dot fr