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.
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
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⟩
