Defining Corecursive Functions in Coq Using Approximations

Rusu, Vlad; Nowak, David

Document type :

Communication dans un congrès avec actes

DOI :

10.4230/LIPIcs.ECOOP.2022.12

Title :

Defining Corecursive Functions in Coq Using Approximations

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]

Conference title :

ECOOP

City :

Berlin

Country :

Allemagne

Start date of the conference :

2022-06-08

Book title :

Proceedings ECOOP 20222, 8-10 Jube 2022, Berlin, Germany.

English keyword(s) :

corecursive function
productiveness
approximation
Coq proof assistant

HAL domain(s) :

Informatique [cs]

English abstract : [en]

We present two methods for defining corecursive functions that go beyond what is accepted by the builtin corecursion mechanisms of the Coq proof assistant. This gain in expressiveness is obtained by using a combination of ...
Show more >We present two methods for defining corecursive functions that go beyond what is accepted by the builtin corecursion mechanisms of the Coq proof assistant. This gain in expressiveness is obtained by using a combination of axioms from Coq's standard library that, to our best knowledge, do not introduce inconsistencies but enable reasoning in standard mathematics. Both methods view corecursive functions as limits of sequences of approximations, and both are based on a property of productiveness that, intuitively, requires that for each input, an arbitrarily close approximation of the corresponding output is eventually obtained. The first method uses Coq's builtin corecursive mechanisms in a non-standard way, while the second method uses none of the mechanisms but redefines them. Both methods are implemented in Coq and are illustrated with examples.Show less >

Language :

Anglais

Peer reviewed article :

Oui

Audience :

Internationale

Popular science :

Non

Collections :

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

Source :

Harvested from HAL

Files

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

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

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

Defining Corecursive Functions in Coq Using ... BibTeX CSV Excel RIS

Files

Defining Corecursive Functions in Coq Using ...

BibTeX

CSV

Excel

RIS