Transferring Arithmetic Decision Procedures (on Z) to Alternative Representations

Nicolas Magaud (1, 2)

1 IGG
2 CAMUS - Compilation pour les Architectures MUlti-coeurS

We propose a generic approach to make arithmetic decision procedures designed for the concrete data-type Z of Coq available for alternative representations of integers. It is based on a transfer tool recently developped by Zimmermann and Herbelin to perform automatic and transparent transfer of theorems along isomorphisms.

Mots clés: Coq; ssreflect; omega

Domaines: Informatique [cs]

Nicolas Magaud. Transferring Arithmetic Decision Procedures (on Z) to Alternative Representations. CoqPL 2017: The Third International Workshop on Coq for Programming Languages, Jan 2017, Paris, France. ⟨hal-01518660⟩