|
Download PDFOpen PDF in browserCurrent versionTowards Corecursion Without Corecursion in CoqEasyChair Preprint 8442, version 111 pages•Date: July 10, 2022AbstractCoinduction is an important concept in functional programming. To formally prove properties of 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 particular, corecursive calls must occur directly under a call to a constructor, without any calls to other recursive functions in between. In this paper we show how a partially ordered set endowed with a notion of approximation can be organized as a Complete Partial Order. This makes it possible to define corecursive functions without using Coq's corecursion, as the unique solution of a fixpoint equation, thereby escaping Coq's builtin limitations. Keyphrases: Coq, coinductive type, corecursive function, fixpoint Download PDFOpen PDF in browserCurrent version |
|
|