Simple simpl

We report on a new implementation of a reduction strategy in Coq to simplify terms during interactive proofs. By "simplify", we mean to reduce terms as much as possible while avoid- ing to make them grow in size. Reaching this goal amounts to a discussion about how not to unfold uselessly global constants. Coq's simpl is such a reduction strategy and the current paper describes an alternative more efficient abstract-machine-based implementation to it

Data and Resources

Additional Info

Field Value
Source https://hal.science/hal-00816918
Author Boutillier, Pierre
Maintainer CCSD
Last Updated May 11, 2026, 08:39 (UTC)
Created May 11, 2026, 08:39 (UTC)
Identifier hal-00816918
Language en
Rights https://about.hal.science/hal-authorisation-v1/
contributor Design, study and implementation of languages for proofs and programs (PI.R2) ; Preuves, Programmes et Systèmes (PPS) ; Université Paris Diderot - Paris 7 (UPD7)-Centre National de la Recherche Scientifique (CNRS)-Université Paris Diderot - Paris 7 (UPD7)-Centre National de la Recherche Scientifique (CNRS)-Inria Paris-Rocquencourt ; Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)
creator Boutillier, Pierre
date 2013-03-29T00:00:00
harvest_object_id 715f679e-4dce-4a39-8591-b3ccedbe86cf
harvest_source_id 3374d638-d20b-4672-ba96-a23232d55657
harvest_source_title test moissonnage SELUNE
metadata_modified 2025-02-26T00:00:00
set_spec type:UNDEFINED