Importing HOL Light into Coq

Chantal Keller 1, 2, 3 Benjamin Werner 1, 2
2 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
Abstract : We present a new scheme to translate mathematical developments from HOL Light to Coq, where they can be re-used and re-checked. By relying on a carefully chosen embedding of Higher-Order Logic into Type Theory, we try to avoid some pitfalls of inter-operation between proof systems. In particular, our translation keeps the mathematical statements intelligible. This translation has been implemented and allows the importation of the HOL Light basic library into Coq.
Type de document :
Communication dans un congrès
Matt Kaufmann and Lawrence C. Paulson. ITP - Interactive Theorem Proving, First International Conference - 2010, Jul 2010, Edimbourg, United Kingdom. Springer, 6172, pp.307-322, 2010, Lecture Notes in Computer Science. 〈http://www.springerlink.com/content/a74714134ut7316n/〉
Liste complète des métadonnées

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

https://hal.inria.fr/inria-00520604
Contributeur : Chantal Keller <>
Soumis le : jeudi 23 septembre 2010 - 17:59:17
Dernière modification le : jeudi 10 mai 2018 - 02:06:51
Document(s) archivé(s) le : jeudi 25 octobre 2012 - 11:25:45

Fichier

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

Identifiants

  • HAL Id : inria-00520604, version 1

Collections

Citation

Chantal Keller, Benjamin Werner. Importing HOL Light into Coq. Matt Kaufmann and Lawrence C. Paulson. ITP - Interactive Theorem Proving, First International Conference - 2010, Jul 2010, Edimbourg, United Kingdom. Springer, 6172, pp.307-322, 2010, Lecture Notes in Computer Science. 〈http://www.springerlink.com/content/a74714134ut7316n/〉. 〈inria-00520604〉

Partager

Métriques

Consultations de la notice

348

Téléchargements de fichiers

224