A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses

Germain Faure 1, 2 Chantal Keller Thery Laurent Gregoire Benjamin Werner Benjamin Armand Mickael
1 TYPICAL - Types, Logic and computing
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France, X - École polytechnique, CNRS - Centre National de la Recherche Scientifique : UMR
Type de document :
Article dans une revue
CERTIFIED PROGRAMS AND PROOFS, Springer, 2011
Liste complète des métadonnées

https://hal.inria.fr/hal-00644216
Contributeur : Germain Faure <>
Soumis le : mercredi 23 novembre 2011 - 18:32:24
Dernière modification le : jeudi 10 mai 2018 - 02:06:34

Identifiants

  • HAL Id : hal-00644216, version 1

Collections

Citation

Germain Faure, Chantal Keller, Thery Laurent, Gregoire Benjamin, Werner Benjamin, et al.. A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses. CERTIFIED PROGRAMS AND PROOFS, Springer, 2011. 〈hal-00644216〉

Partager

Métriques

Consultations de la notice

214