@incollection{'MC6',
title = { {Coq} },
author = {Monin, Jean-Fran\c{c}ois and Chavin, Philippe},
month = {APR},
year = {2006},
booktitle = {{Software Specification Methods, An Overview Using a Case Study}},
chapter = {16},
publisher = {Herm\`es Science},
series = {ISTE},
team = {PACSS},
abstract = {This chapter is an attempt to provide a formal specification which is as faithful as possible to the informal one and consistent. The features of Coq are powerful enough to make the specification both very abstract and executable. We \emph{construct} mathematical structures or functions whenever possible, instead of specifying them with axioms. If the axiomatic way turns out better, we look for structures satisfying the axioms we need.},
}
