Mixing HOL and Coq in Dedukti (Rough Diamond)

Abstract : We use Dedukti as a logical framework for interoperability. We use automated tools to translate different developments made in HOL and in Coq to Dedukti and we combine them to prove new results.
Type de document :
Pré-publication, Document de travail
2015
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01141789
Contributeur : Ali Assaf <>
Soumis le : lundi 13 avril 2015 - 17:13:32
Dernière modification le : jeudi 13 septembre 2018 - 15:24:07
Document(s) archivé(s) le : mardi 18 avril 2017 - 17:52:18

Fichier

dedukti-interop.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01141789, version 1

Citation

Ali Assaf, Raphaël Cauderlier. Mixing HOL and Coq in Dedukti (Rough Diamond). 2015. 〈hal-01141789〉

Partager

Métriques

Consultations de la notice

198

Téléchargements de fichiers

68