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
Type de document :
Communication dans un congrès
CoqPL 2017: The Third International Workshop on Coq for Programming Languages, Jan 2017, Paris, France. 〈http://conf.researchr.org/track/CoqPL-2017/main〉. 〈10.1145/nnnnnnn.nnnnnnn〉
Liste complète des métadonnées

Littérature citée [11 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01518660
Contributeur : Nicolas Magaud <>
Soumis le : vendredi 5 mai 2017 - 10:52:52
Dernière modification le : jeudi 29 mars 2018 - 09:10:05
Document(s) archivé(s) le : dimanche 6 août 2017 - 12:14:36

Fichier

ssr_omega.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

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. 〈http://conf.researchr.org/track/CoqPL-2017/main〉. 〈10.1145/nnnnnnn.nnnnnnn〉. 〈hal-01518660〉

Partager

Métriques

Consultations de la notice

92

Téléchargements de fichiers

38