Le Teaser (work in progress)
Pierre Castéran
About this project
Objective
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 :
- A bunch of chapters, each one dedicated to some domain of application,
whose development in Coq allows us to present various techniques.
- The .v files that accompany the text
- A set of exercises, of graded difficulty.
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.
Draft
Email : pierre dot casteran at labri dot fr