Coq in a Hurry
计算机科学中的逻辑
2008-11-07 v3
摘要
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.
引用
@article{arxiv.cs/0603118,
title = {Coq in a Hurry},
author = {Yves Bertot},
journal= {arXiv preprint arXiv:cs/0603118},
year = {2008}
}