Coq in a Hurry
Yves Bertot (INRIA Sophia Antipolis)
TL;DR
This paper offers a concise tutorial on using the Coq proof assistant for defining logical concepts, functions, and reasoning, enabling quick experimentation for learners.
Contribution
It provides a beginner-friendly, quick-start guide to Coq, focusing on practical usage rather than exhaustive coverage.
Findings
Easy-to-follow introduction to Coq's capabilities
Guidance for rapid experimentation with logical concepts
Foundation for further detailed study and exercises
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Mathematics, Computing, and Information Processing