Towards Corecursion Without Corecursion in Coq

Rusu, Vlad; Nowak, David

Type de document :

Pré-publication ou Document de travail

URL permanente :

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

Titre :

Towards Corecursion Without Corecursion in Coq

Auteur(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]

Discipline(s) HAL :

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

Résumé en anglais : [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 ...
Lire la suite >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.Lire moins >

Langue :

Anglais

Collections :

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

Source :

Harvested from HAL

Date de dépôt :

2022-06-09T02:07:43Z

Fichiers

https://hal.inria.fr/hal-03689027/document
Accès libre
Accéder au document

Towards Corecursion Without Corecursion in Coq BibTeX CSV Excel RIS

Fichiers

Towards Corecursion Without Corecursion in Coq

BibTeX

CSV

Excel

RIS