https://hal.inria.fr/hal-01414881Cohen, CyrilCyrilCohenMARELLE - Mathematical, Reasoning and Software - CRISAM - Inria Sophia Antipolis - Méditerranée - Inria - Institut National de Recherche en Informatique et en AutomatiqueRouhling, DamienDamienRouhlingMARELLE - Mathematical, Reasoning and Software - CRISAM - Inria Sophia Antipolis - Méditerranée - Inria - Institut National de Recherche en Informatique et en AutomatiqueA refinement-based approach to large scale reflection for algebraHAL CCSD2017[INFO] Computer Science [cs][INFO.INFO-LO] Computer Science [cs]/Logic in Computer Science [cs.LO][INFO.INFO-MS] Computer Science [cs]/Mathematical Software [cs.MS]Rouhling, Damien2016-12-12 16:18:242022-06-25 23:24:392016-12-12 16:57:03enConference papersapplication/pdf1Large 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].