Coinductive

Andreas Lochbihler 🌐 with contributions from Johannes Hölzl 📧

February 12, 2010

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.

Abstract

This article collects formalisations of general-purpose coinductive data types and sets. Currently, it contains coinductive natural numbers, coinductive lists, i.e. lazy lists or streams, infinite streams, coinductive terminated lists, coinductive resumptions, a library of operations on coinductive lists, and a version of König's lemma as an application for coinductive lists.
The initial theory was contributed by Paulson and Wenzel. Extensions and other coinductive formalisations of general interest are welcome.
BSD License

Topics

Theories of Coinductive

Used by

Cite

× 
@article{Coinductive-AFP,
  author  = {Andreas Lochbihler},
  title   = {Coinductive},
  journal = {Archive of Formal Proofs},
  month   = February,
  year    = 2010,
  note    = {\url{https://isa-afp.org/entries/Coinductive.html},
            Formal proof development},
  ISSN    = {2150-914x},
}
Download

Download

× Download latest