Skip to Main content Skip to Navigation
New interface
Conference papers

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].
Complete list of metadata

Cited literature [9 references]  Display  Hide  Download
Contributor : Damien Rouhling Connect in order to contact the contributor
Submitted on : Monday, December 12, 2016 - 4:18:24 PM
Last modification on : Saturday, June 25, 2022 - 11:24:39 PM
Long-term archiving on: : Monday, March 27, 2017 - 8:54:06 PM


Files produced by the author(s)


  • HAL Id : hal-01414881, version 1



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⟩



Record views


Files downloads