Equations reloaded - Archive ouverte HAL Access content directly
Journal Articles Proceedings of the ACM on Programming Languages Year : 2019

Equations reloaded

(1, 2) , (1, 2)
1
2

Abstract

Equations is a plugin for the Coq proof assistant which provides a notation for defining programs by dependent pattern-matching and structural or well-founded recursion. It additionally derives useful proof principles for demonstrating properties about them. We present a general design and implementation that provides a robust and expressive function definition package as a definitional extension to the Coq kernel. At the core of the system is a new simplifier for dependent equalities that can be reused to define enhanced versions of dependent elimination tactics. We introduce verified optimizations of the simplifier that allow generating smaller and simpler Equations definitions and proof terms for these tactics in general.
Fichier principal
Vignette du fichier
icfp19main-p204-p.pdf (632.7 Ko) Télécharger le fichier
Origin : Files produced by the author(s)
Loading...

Dates and versions

hal-01671777 , version 1 (22-12-2017)
hal-01671777 , version 2 (15-12-2018)
hal-01671777 , version 3 (09-12-2019)

Identifiers

Cite

Matthieu Sozeau, Cyprien Mangin. Equations reloaded. Proceedings of the ACM on Programming Languages, 2019, 3 (ICFP), pp.1-29. ⟨10.1145/3341690⟩. ⟨hal-01671777v3⟩
370 View
344 Download

Altmetric

Share

Gmail Facebook Twitter LinkedIn More