Towards Corecursion Without Corecursion in Coq

EasyChair Preprint no. 8442, version history

VersionDatePagesVersion notes
1July 10, 202211
2August 15, 202222

All pending results in the previous version are proved.

Keyphrases: coinductive type, Coq, corecursive function, fixpoint

BibTeX entry
BibTeX does not have the right entry for preprints. This is a hack for producing the correct reference:
  author = {Vlad Rusu and David Nowak},
  title = {Towards Corecursion Without Corecursion in Coq},
  howpublished = {EasyChair Preprint no. 8442},

  year = {EasyChair, 2022}}