An ad-hoc and monolithic method for ensuring that corecursive definitions are productiveAn ad-hoc and monolithic method for ensuring that corecursive definitions are productive AbstractCorecursion 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. Nils Anders DanielssonLast updated Tue Jan 20 11:15:05 UTC 2009. |