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 metadata

Cited literature [9 references] Display Hide Download

https://hal.inria.fr/hal-01518660
Contributor : Nicolas Magaud Connect in order to contact the contributor
Submitted on : Friday, May 5, 2017 - 10:52:52 AM
Last modification on : Thursday, December 2, 2021 - 3:17:01 AM
Long-term archiving on: : Sunday, August 6, 2017 - 12:14:36 PM

Transferring Arithmetic Decision Procedures (on Z) to Alternative Representations

File

Identifiers

Collections

Citation

Export

Metrics

Contact Legal Notice Personal Data

Transferring Arithmetic Decision Procedures (on Z) to Alternative Representations

File

Identifiers

Collections

Citation

Export

Share

Metrics

Contact Legal Notice Personal Data