| 000 | 05018nam a2201201 i 4500 | ||
|---|---|---|---|
| 001 | 6712486 | ||
| 003 | IEEE | ||
| 005 | 20220712204818.0 | ||
| 006 | m o d | ||
| 007 | cr |n||||||||| | ||
| 008 | 151229s2013 mau ob 001 eng d | ||
| 010 | _z 2013012837 (print) | ||
| 020 |
_z9780262026659 _qhardback |
||
| 020 |
_a9780262317870 _qelectronic |
||
| 020 | _a9780262026659 | ||
| 020 |
_z0262026651 _qhardcover : alk. paper |
||
| 035 | _a(CaBNVSL)mat06712486 | ||
| 035 | _a(IDAMS)0b00006481ff4d7a | ||
| 040 |
_aCaBNVSL _beng _erda _cCaBNVSL _dCaBNVSL |
||
| 050 | 4 |
_aQA76.9.A96 _bC45 2013eb |
|
| 082 | 0 | 0 |
_a005.1 _223 |
| 100 | 1 |
_aChlipala, Adam, _d1981- _924199 |
|
| 245 | 1 | 0 |
_aCertified programming with dependent types : _ba pragmatic introduction to the Coq proof assistant / _cAdam Chlipala. |
| 264 | 1 |
_aCambridge, Massachusetts : _bMIT Press, _c[2013] |
|
| 264 | 2 |
_a[Piscataqay, New Jersey] : _bIEEE Xplore, _c[2013] |
|
| 300 | _a1 PDF (xii, 424 pages). | ||
| 336 |
_atext _2rdacontent |
||
| 337 |
_aelectronic _2isbdmedia |
||
| 338 |
_aonline resource _2rdacarrier |
||
| 504 | _aIncludes bibliographical references and index. | ||
| 506 | 1 | _aRestricted to subscribers or individual electronic text purchasers. | |
| 520 | _aThe technology of mechanized program verification can play a supporting role in many kinds of research projects in computer science, and related tools for formal proof-checking are seeing increasing adoption in mathematics and engineering. This book provides an introduction to the Coq software for writing and checking mathematical proofs. It takes a practical engineering focus throughout, emphasizing techniques that will help users to build, understand, and maintain large Coq developments and minimize the cost of code change over time. Two topics, rarely discussed elsewhere, are covered in detail: effective dependently typed programming (making productive use of a feature at the heart of the Coq system) and construction of domain-specific proof tactics. Almost every subject covered is also relevant to interactive computer theorem proving in general, not just program verification, demonstrated through examples of verified programs applied in many different sorts of formalizations. The book develops a unique automated proof style and applies it throughout; even experienced Coq users may benefit from reading about basic Coq concepts from this novel perspective. The book also offers a library of tactics, or programs that find proofs, designed for use with examples in the book. Readers will acquire the necessary skills to reimplement these tactics in other settings by the end of the book. All of the code appearing in the book is freely available online. | ||
| 530 | _aAlso available in print. | ||
| 538 | _aMode of access: World Wide Web | ||
| 588 | _aDescription based on PDF viewed 12/29/2015. | ||
| 630 | 0 | 0 |
_aCoq (Electronic resource) _924200 |
| 650 | 0 |
_aComputer programming. _94169 |
|
| 650 | 0 |
_aAutomatic theorem proving _xComputer programs. _924201 |
|
| 655 | 0 |
_aElectronic books. _93294 |
|
| 695 | _aAbstracts | ||
| 695 | _aAlgorithm design and analysis | ||
| 695 | _aAntenna measurements | ||
| 695 | _aAntenna radiation patterns | ||
| 695 | _aArrays | ||
| 695 | _aAutomation | ||
| 695 | _aAzimuth | ||
| 695 | _aBinary trees | ||
| 695 | _aBuildings | ||
| 695 | _aBusiness | ||
| 695 | _aCalculus | ||
| 695 | _aCognition | ||
| 695 | _aColon | ||
| 695 | _aComputer bugs | ||
| 695 | _aComputer languages | ||
| 695 | _aContext | ||
| 695 | _aData structures | ||
| 695 | _aElectronic mail | ||
| 695 | _aEncoding | ||
| 695 | _aFeature extraction | ||
| 695 | _aFocusing | ||
| 695 | _aFunctional programming | ||
| 695 | _aIndexes | ||
| 695 | _aKernel | ||
| 695 | _aLaw | ||
| 695 | _aLength measurement | ||
| 695 | _aLibraries | ||
| 695 | _aLogic programming | ||
| 695 | _aManuals | ||
| 695 | _aMaterials | ||
| 695 | _aMathematics | ||
| 695 | _aMemory management | ||
| 695 | _aMetals | ||
| 695 | _aMirrors | ||
| 695 | _aPattern matching | ||
| 695 | _aPragmatics | ||
| 695 | _aPresses | ||
| 695 | _aPrinting | ||
| 695 | _aProductivity | ||
| 695 | _aProgram processors | ||
| 695 | _aProgramming | ||
| 695 | _aRadio access networks | ||
| 695 | _aRadio frequency | ||
| 695 | _aReactive power | ||
| 695 | _aRegisters | ||
| 695 | _aSections | ||
| 695 | _aSemantics | ||
| 695 | _aSet theory | ||
| 695 | _aSize measurement | ||
| 695 | _aSoftware | ||
| 695 | _aStandards | ||
| 695 | _aStreaming media | ||
| 695 | _aSugar | ||
| 695 | _aSurface treatment | ||
| 695 | _aSurges | ||
| 695 | _aSwitches | ||
| 695 | _aSyntactics | ||
| 695 | _aWriting | ||
| 710 | 2 |
_aIEEE Xplore (Online Service), _edistributor. _924202 |
|
| 710 | 2 |
_aMIT Press, _epublisher. _924203 |
|
| 776 | 0 | 8 |
_iPrint version: _z9780262026659 |
| 856 | 4 | 2 |
_3Abstract with links to resource _uhttps://ieeexplore.ieee.org/xpl/bkabstractplus.jsp?bkn=6712486 |
| 942 | _cEBK | ||
| 999 |
_c73349 _d73349 |
||