%0 Journal Article %1 citeulike:14251821 %A Bertot, Yves %D 2010 %K 03-04-mathematical-logic-and-foundations-machine-computation-and-programs, coq 03b35-mechanization-of-proofs-and-logical-operations %T Coq in a Hurry %U https://cel.archives-ouvertes.fr/inria-00001173\#.WHn14azcm6A.citeulike %X 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. %7 Third Cycle

@article{citeulike:14251821, abstract = {{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.}}, added-at = {2017-06-29T07:13:07.000+0200}, author = {Bertot, Yves}, biburl = {https://www.bibsonomy.org/bibtex/244f38f5d0e2f858221b7a4a83a04d507/gdmcbain}, citeulike-article-id = {14251821}, citeulike-attachment-1 = {bertot_10_coq.pdf; /pdf/user/gdmcbain/article/14251821/1097990/bertot_10_coq.pdf; a4769483fa8a82ae6f25dc88ad221abc1d74dbe6}, citeulike-linkout-0 = {https://cel.archives-ouvertes.fr/inria-00001173\#.WHn14azcm6A.citeulike}, edition = {Third Cycle}, file = {bertot_10_coq.pdf}, howpublished = {3rd cycle. Types Summer School, also used at the University of Goteborg, Nice, Ecole Jeunes Chercheurs en Programmation, Universite de Nice, 2010, pp.43}, interhash = {bc9f01811ec497a5c28f74003fc58e0e}, intrahash = {44f38f5d0e2f858221b7a4a83a04d507}, keywords = {03-04-mathematical-logic-and-foundations-machine-computation-and-programs, coq 03b35-mechanization-of-proofs-and-logical-operations}, posted-at = {2017-01-14 09:58:47}, priority = {2}, timestamp = {2021-01-14T05:05:02.000+0100}, title = {{Coq in a Hurry}}, url = {https://cel.archives-ouvertes.fr/inria-00001173\#.WHn14azcm6A.citeulike}, year = 2010 }