Développement de l'algorithme d'unification dans le calcul des constructions avec types inductifs

Résumé : On trouve dans cet article une traduction possible de la notion de termes et de substitution dans le calcul des constructions avec types inductifs et une preuve constructive de l'unification au premier ordre de laquelle on peut extraire un algorithme (proche de celui de Robinson). Le logiciel utilise pour le codage et la vérification des preuves est le Coq Proof Assistant version 5.6. L'article est conçu pour une lecture en parallèle du code en Coq et de la transcription qui en est faite en langage mathématique. Il a été écrit également dans le but d'aider ceux qui le désirent à pénétrer rapidement dans le monde du calcul des constructions.
Type de document :
Rapport
[Rapport de recherche] RR-1795, INRIA. 1992
Liste complète des métadonnées

https://hal.inria.fr/inria-00077035
Contributeur : Rapport de Recherche Inria <>
Soumis le : lundi 29 mai 2006 - 11:56:43
Dernière modification le : samedi 17 septembre 2016 - 01:06:54
Document(s) archivé(s) le : vendredi 13 mai 2011 - 22:40:18

Fichiers

Identifiants

  • HAL Id : inria-00077035, version 1

Collections

Citation

Joseph Rouyer. Développement de l'algorithme d'unification dans le calcul des constructions avec types inductifs. [Rapport de recherche] RR-1795, INRIA. 1992. 〈inria-00077035〉

Partager

Métriques

Consultations de la notice

259

Téléchargements de fichiers

78