Journal Article: Coinductive

[lochbihler10afp]

Andreas Lochbihler, Coinductive, Archive of Formal Proofs, February 2010. Formal proof development

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, and a library of operations on coinductive lists. The initial theory was contributed by Paulson and Wenzel. Extensions and other coinductive formalisations of general interest are welcome.

Download

[Link]

BibTeX

@article{lochbihler10afp,
  title = {Coinductive},
  year = {2010},
  month = feb,
  journal = {Archive of Formal Proofs},
  author = {Andreas Lochbihler},
  note = {Formal proof development},
  url = {http://afp.sf.net/entries/Coinductive.shtml},
}

Authors at the institute

Former Staff Member
Dr. rer. nat. Andreas Lochbihler

Projects

Project

Quis-Custodiet