Simple simpl

Pierre Boutillier (1, 2)

1 PI.R2 - Design, study and implementation of languages for proofs and programs
2 PPS - Preuves, Programmes et Systèmes

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

Mots clés: Coq; Krivine Abstract Machine; Algebraic datatypes; Reduction strategy

Domaines: Logiciel mathématique [cs.MS]; Langage de programmation [cs.PL]

Pierre Boutillier. Simple simpl. 2013. ⟨hal-00816918⟩