Coq in a Hurry Export

@article{citeulike:3501167, abstract = {These notes provide a quick introduction to the Coq system and show how it can be used to define logical concepts and functions and reason about them. It is designed as a tutorial, so that readers can quickly start their own experiments, learning only a few of the capabilities of the system. A much more comprehensive study is provided in [1], which also provides an extensive collection of exercises to train on.}, archivePrefix = {arXiv}, author = {Bertot, Yves}, citeulike-article-id = {3501167}, citeulike-linkout-0 = {http://arxiv.org/abs/cs/0603118}, citeulike-linkout-1 = {http://arxiv.org/pdf/cs/0603118}, day = {7}, eprint = {cs/0603118}, keywords = {2005, coq, proof}, month = {Nov}, posted-at = {2009-02-16 01:43:11}, priority = {2}, title = {Coq in a Hurry}, url = {http://arxiv.org/abs/cs/0603118}, year = {2008} }

TY - JOUR ID - citeulike:3501167 L3 - citeulike-article-id:3501167 N2 - These notes provide a quick introduction to the Coq system and show how it can be used to define logical concepts and functions and reason about them. It is designed as a tutorial, so that readers can quickly start their own experiments, learning only a few of the capabilities of the system. A much more comprehensive study is provided in [1], which also provides an extensive collection of exercises to train on. TI - Coq in a Hurry KW - 2005 KW - coq KW - proof AU - Bertot, Yves PY - 2008/Nov/07/ UR - http://arxiv.org/abs/cs/0603118 ER -