Towards Corecursion Without Corecursion in Coq

Rusu, Vlad; Nowak, David

Document type :

Pré-publication ou Document de travail

Permalink :

http://hdl.handle.net/20.500.12210/74810

Title :

Towards Corecursion Without Corecursion in Coq

Author(s) :

Rusu, Vlad [Auteur]

Analyse symbolique et conception orientée composants pour des systèmes embarqués temps-réel modulaires [SYCOMORES]
Nowak, David [Auteur]

Extra Small Extra Safe [2XS]

HAL domain(s) :

Informatique [cs]/Génie logiciel [cs.SE]

English abstract : [en]

Coinduction 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 ...
Show more >Coinduction 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.Show less >

Language :

Anglais

Collections :

Centre de Recherche en Informatique, Signal et Automatique de Lille (CRIStAL) - UMR 9189

Source :

Harvested from HAL

Submission date :

2022-06-09T02:07:43Z

Files

https://hal.inria.fr/hal-03689027/document
Open access
Access the document

Towards Corecursion Without Corecursion in Coq BibTeX CSV Excel RIS

Files

Towards Corecursion Without Corecursion in Coq

BibTeX

CSV

Excel

RIS