Vlad Rusu
Inria, Lille, France

Corecursive functions are, informally speaking, functions whose normal behaviour includes non- termination. They naturally occur in synchronous and in lazy programming languages. In order to formally reason about corecursive functions one can try to define them in a proof assistant such as Coq. But there are limitations on the functions that can be defined in this way: corecursive calls must be guarded - they may only occur directly under a call to a constructor of the function’s codomain. Coinductive proofs have to satisfy a similar requirement. In this talk I shall present an approach for defining and reasoning about corecursive functions in Coq beyond the guarded fragment.