CoInduction in Coq
Yves Bertot (INRIA Sophia Antipolis)
TL;DR
This paper explains co-induction in Coq and demonstrates its application in proving properties of real number representations.
Contribution
It provides an overview of co-induction in Coq and applies it to arithmetic properties of simple real number representations.
Findings
Co-induction concepts in Coq are clarified.
Arithmetic properties of real numbers are established.
Practical application of co-induction in formal proofs.
Abstract
We describe the basic notions of co-induction as they are available in the coq system. As an application, we describe arithmetic properties for simple representations of real numbers.
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 · semigroups and automata theory · Polynomial and algebraic computation