Skip to Main content Skip to Navigation
New interface
Conference papers

Élimination des quantificateurs sur les réels pour Coq

Assia Mahboubi 1, 2 Loïc Pottier 1 
Résumé : On présente ici l'implémentation en OCaml d'une tactique Coq qui réalise une procédure d'élimination des quantificateurs pour les réels, basée sur la méthode de Hormander.
Document type :
Conference papers
Complete list of metadata

https://hal.inria.fr/hal-00819482
Contributor : Assia Mahboubi Connect in order to contact the contributor
Submitted on : Wednesday, May 1, 2013 - 3:49:46 PM
Last modification on : Friday, February 4, 2022 - 3:12:32 AM
Long-term archiving on: : Friday, August 2, 2013 - 4:05:58 AM

Files

jfla02.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-00819482, version 1

Collections

Citation

Assia Mahboubi, Loïc Pottier. Élimination des quantificateurs sur les réels pour Coq. Journées Francophones des Langages Applicatifs, Jan 2002, Anglet, France. ⟨hal-00819482⟩

Share

Metrics

Record views

165

Files downloads

78