A refinement-based approach to large scale reflection for algebra

Cyril Cohen 1 Damien Rouhling 1
1 MARELLE - Mathematical, Reasoning and Software
CRISAM - Inria Sophia Antipolis - Méditerranée
Abstract : Large scale reflection tactics are often implemented with ad-hoc data-structures and in a way which is specific to the problematic. This makes it hard to add improvements and to implement variations without writing an extensive theory of the specific data-structures involved. We suggest to replace the core of such tactics with procedures that are proven correct using CoqEAL refinement framework, and to build a modular methodology around it. This refinement framework addresses the problem of duplication by promoting the use of one extensive proof-oriented library together with one or several more efficient implementations, with a reduced amount of proofs, but destined to computation and proven correct with regard to the proof-oriented library. We show on the example of the ring tactic of Coq that this gain in flexibility opens the door to different improvements. This is a presentation to trigger discussion about ideas for a prototype based on the existing but improved CoqEAL refinement framework, described in [5] and [3].
Type de document :
Communication dans un congrès
JFLA 2017 - Vingt-huitième Journées Francophones des Langages Applicatifs, Jan 2017, Gourette, France
Liste complète des métadonnées

Littérature citée [9 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01414881
Contributeur : Damien Rouhling <>
Soumis le : lundi 12 décembre 2016 - 16:18:24
Dernière modification le : jeudi 11 janvier 2018 - 16:47:58
Document(s) archivé(s) le : lundi 27 mars 2017 - 20:54:06

Fichier

cyrilcohen.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01414881, version 1

Citation

Cyril Cohen, Damien Rouhling. A refinement-based approach to large scale reflection for algebra. JFLA 2017 - Vingt-huitième Journées Francophones des Langages Applicatifs, Jan 2017, Gourette, France. 〈hal-01414881〉

Partager

Métriques

Consultations de la notice

218

Téléchargements de fichiers

86