An ad-hoc and monolithic method for ensuring that corecursive definitions are productive

An ad-hoc and monolithic method for ensuring that corecursive definitions are productive
Agda Intensive Meeting 9, Sendai, 2008-11-27. (Slightly edited.) For more information, see Beating the Productivity Checker Using Embedded Languages. [pdf, pdf (n-up)]

Abstract

Corecursion is a nice and elegant method for dealing with infinite objects, at least when it works. Unfortunately it is sometimes hard to cast corecursive definitions in a form which is accepted by systems like Coq and Agda, which require corecursive definitions to be guarded by constructors. I will present an ad-hoc and monolithic method for ensuring that corecursive definitions are accepted by Agda. The method, which is both useful and awkward, amounts to defining a problem-specific programming language along with a provably productive interpreter.