Transferring Arithmetic Decision Procedures (on Z) to Alternative Representations

Nicolas Magaud

doi:10.1145/nnnnnnn.nnnnnnn

Conference papers

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

Domain :

Computer Science [cs]

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
Document(s) archivé(s) le : Sunday, August 6, 2017 - 12:14:36 PM

ssr_omega.pdf

Files produced by the author(s)

Transferring Arithmetic Decision Procedures (on Z) to Alternative Representations

File

Identifiers

Collections

Citation

Export

Metrics

239

140

Contact Legal Notice Personal Data

Transferring Arithmetic Decision Procedures (on Z) to Alternative Representations

File

Identifiers

Collections

Citation

Export

Share

Metrics

239

140

Contact Legal Notice Personal Data