Defining Corecursive Functions in Coq Using ...
Type de document :
Communication dans un congrès avec actes
Titre :
Defining Corecursive Functions in Coq Using Approximations
Auteur(s) :
Rusu, Vlad [Auteur]
Analyse symbolique et conception orientée composants pour des systèmes embarqués temps-réel modulaires [SYCOMORES]
Nowak, David [Auteur]
Extra Small Extra Safe [2XS]
Centre de Recherche en Informatique, Signal et Automatique de Lille - UMR 9189 [CRIStAL]
Analyse symbolique et conception orientée composants pour des systèmes embarqués temps-réel modulaires [SYCOMORES]
Nowak, David [Auteur]
Extra Small Extra Safe [2XS]
Centre de Recherche en Informatique, Signal et Automatique de Lille - UMR 9189 [CRIStAL]
Titre de la manifestation scientifique :
ECOOP
Ville :
Berlin
Pays :
Allemagne
Date de début de la manifestation scientifique :
2022-06-08
Titre de l’ouvrage :
Proceedings ECOOP 20222, 8-10 Jube 2022, Berlin, Germany.
Mot(s)-clé(s) en anglais :
corecursive function
productiveness
approximation
Coq proof assistant
productiveness
approximation
Coq proof assistant
Discipline(s) HAL :
Informatique [cs]
Résumé en anglais : [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 ...
Lire la suite >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.Lire moins >
Lire la suite >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.Lire moins >
Langue :
Anglais
Comité de lecture :
Oui
Audience :
Internationale
Vulgarisation :
Non
Collections :
Source :
Fichiers
- https://hal.inria.fr/hal-03671876/document
- Accès libre
- Accéder au document
- https://hal.inria.fr/hal-03671876/document
- Accès libre
- Accéder au document
- https://hal.inria.fr/hal-03671876/document
- Accès libre
- Accéder au document
- document
- Accès libre
- Accéder au document
- final.pdf
- Accès libre
- Accéder au document