Foundational Extensible Corecursion -- A Proof Assistant Perspective

This paper presents a formalized framework for defining corecursive functions safely in a total setting, based on corecursion up-to and relational parametricity. The end product is a general core-cursor that allows corecursive (and even recursive) calls under “friendly ” operations, including constructors. Friendly corecursive functions can be registered as such, thereby increasing the corecur-sor’s expressiveness. The metatheory is formalized in the Isabelle proof assistant and forms the core of a prototype tool. The corecur-sor is derived from first principles, without requiring new axioms or extensions of the logic