Using structural recursion for corecursion

Research output: Chapter in Book/Report/Conference proceedingChapter

5 Citations (Scopus)


We propose a (limited) solution to the problem of constructing stream values defined by recursive equations that do not respect the guardedness condition. The guardedness condition is imposed on definitions of corecursive functions in Coq, AGDA, and other higher-order proof assistants. In this paper, we concentrate in particular on those non-guarded equations where recursive calls appear under functions. We use a correspondence between streams and functions over natural numbers to show that some classes of non-guarded definitions can be modelled through the encoding as structural recursive functions. In practice, this work extends the class of stream values that can be defined in a constructive type theory-based theorem prover with inductive and coinductive types, structural recursion and guarded corecursion.
Original languageEnglish
Title of host publicationTypes for Proofs and Programs
Subtitle of host publicationInternational Conference, TYPES 2008 Torino, Italy, March 26-29, 2008 Revised Selected Papers
EditorsStefano Berardi, Ferruccio Damiani, Ugo de’Liguoro
Number of pages17
ISBN (Electronic)9783642024443
ISBN (Print)9783642024436
Publication statusPublished - 2009

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Berlin Heidelberg
ISSN (Print)0302-9743


  • Constructive Type Theory
  • Structural Recursion
  • Coinductive types
  • Guarded Corecursion
  • Coq


Dive into the research topics of 'Using structural recursion for corecursion'. Together they form a unique fingerprint.

Cite this