Transferring Arithmetic Decision Procedures (on Z) to Alternative Representations

Nicolas Magaud 1, 2
1 IGG
ICube - Laboratoire des sciences de l'ingénieur, de l'informatique et de l'imagerie
2 CAMUS - Compilation pour les Architectures MUlti-coeurS
Inria Nancy - Grand Est, ICube - Laboratoire des sciences de l'ingénieur, de l'informatique et de l'imagerie
Abstract : 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.
Keywords : Coq ssreflect omega
Document type :
Conference papers
Complete list of metadatas

Cited literature [9 references]  Display  Hide  Download

https://hal.inria.fr/hal-01518660
Contributor : Nicolas Magaud <>
Submitted on : Friday, May 5, 2017 - 10:52:52 AM
Last modification on : Saturday, October 27, 2018 - 1:23:58 AM
Long-term archiving on : Sunday, August 6, 2017 - 12:14:36 PM

File

ssr_omega.pdf
Files produced by the author(s)

Identifiers

Citation

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. ⟨10.1145/nnnnnnn.nnnnnnn⟩. ⟨hal-01518660⟩

Share

Metrics

Record views

225

Files downloads

130