A Tutorial on Recursive Types in Coq Export

@techreport{gimenez-98, 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.}, author = {Gim\'{e}nez, Eduardo}, citeulike-article-id = {6074215}, citeulike-linkout-0 = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.41.7439}, journal = {INRIA ROCQUENCOURT}, keywords = {coinduction, coq, functional-programming, logic, master-project, recursion, types}, posted-at = {2009-11-05 13:34:58}, priority = {2}, title = {A Tutorial on Recursive Types in Coq}, url = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.41.7439}, year = {1998} }

TY - RPRT ID - gimenez-98 L3 - citeulike-article-id:6074215 N2 - 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. JF - INRIA ROCQUENCOURT TI - A Tutorial on Recursive Types in Coq KW - coinduction KW - coq KW - functional-programming KW - logic KW - master-project KW - recursion KW - types AU - Giménez, Eduardo PY - 1998/// UR - http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.41.7439 ER -