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 metadatas

Cited literature [9 references]  Display  Hide  Download

https://hal.inria.fr/hal-01414881
Contributor : Damien Rouhling <>
Submitted on : Monday, December 12, 2016 - 4:18:24 PM
Last modification on : Thursday, January 11, 2018 - 4:47:58 PM
Long-term archiving on : Monday, March 27, 2017 - 8:54:06 PM

File

cyrilcohen.pdf
Files produced by the author(s)

Identifiers

  • 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⟩

Share

Metrics

Record views

256

Files downloads

121