| HAL-Inria | Publications, software ... of Inria's scientists |
Conference papers
Transferring Arithmetic Decision Procedures (on Z) to Alternative Representations
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.
Cited literature [9 references]
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
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)