Transferring Arithmetic Decision Procedures (on Z) to Alternative Representations - Archive ouverte HAL Access content directly
Conference Papers Year :

Transferring Arithmetic Decision Procedures (on Z) to Alternative Representations

(1, 2)
1
2

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

Fichier principal
Vignette du fichier
ssr_omega.pdf (140.32 Ko) Télécharger le fichier
Origin : Files produced by the author(s)
Loading...

Dates and versions

hal-01518660 , version 1 (05-05-2017)

Identifiers

  • HAL Id : hal-01518660 , version 1

Cite

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. ⟨hal-01518660⟩
156 View
129 Download

Share

Gmail Facebook Twitter LinkedIn More