Skip to Main content Skip to Navigation
Reports

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.
Document type :
Reports
Complete list of metadata

https://hal.inria.fr/inria-00077035
Contributor : Rapport de Recherche Inria <>
Submitted on : Monday, May 29, 2006 - 11:56:43 AM
Last modification on : Thursday, February 11, 2021 - 2:48:31 PM
Long-term archiving on: : Friday, May 13, 2011 - 10:40:18 PM

Identifiers

  • 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⟩

Share

Metrics

Record views

296

Files downloads

120