HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation
Reports

A Tutorial on Recursive Types in Coq

Abstract : This document is an introduction to the definition and use of recursive types in the Coq proof environment. It explains how recursive types like natural numbers and infinite streams are defined in Coq, and the kind of proof techniques that can be used to reason about them (case analysis, induction, inversion of predicates, co-induction, etc). Each technique is illustrated through an executable and self-contained Coq script.
Document type :
Reports
Complete list of metadata

Cited literature [7 references]  Display  Hide  Download

https://hal.inria.fr/inria-00069950
Contributor : Rapport de Recherche Inria Connect in order to contact the contributor
Submitted on : Friday, May 19, 2006 - 6:41:39 PM
Last modification on : Friday, February 4, 2022 - 3:10:18 AM
Long-term archiving on: : Sunday, April 4, 2010 - 7:47:23 PM

Identifiers

  • HAL Id : inria-00069950, version 1

Collections

Citation

Eduardo Giménez. A Tutorial on Recursive Types in Coq. [Research Report] RT-0221, INRIA. 1998, pp.42. ⟨inria-00069950⟩

Share

Metrics

Record views

155

Files downloads

907