Vérification de l'équivalence du $\pi$-calcul dans HOL

Résumé : Dans ce rapport, on décrit une représentation purement définitionnelle du $\pi$-calcul dans le prouveur de théorèmes HOL. Les lois algébriques du $\pi$-calcul sont montrées comme étant des théorèmes dans la logique d'ordre supérieur. Ainsi, on obtient un outil correcte dans lequel on peut raisonner sur des applications utilisant le $\pi$-calcul comme outil de spécification. Comme application, on montre par induction la correction de la spécification de l'addition naturelle en $\pi$-calcul.
keyword : $\pi$-calcul HOL
Type de document :
Rapport
[Rapport de recherche] RR-2412, INRIA. 1994
Liste complète des métadonnées

https://hal.inria.fr/inria-00074263
Contributeur : Rapport de Recherche Inria <>
Soumis le : mercredi 24 mai 2006 - 14:53:43
Dernière modification le : samedi 17 septembre 2016 - 01:06:52
Document(s) archivé(s) le : lundi 5 avril 2010 - 00:07:28

Fichiers

Identifiants

  • HAL Id : inria-00074263, version 1

Collections

Citation

Otmane Ait-Mohamed. Vérification de l'équivalence du $\pi$-calcul dans HOL. [Rapport de recherche] RR-2412, INRIA. 1994. 〈inria-00074263〉

Partager

Métriques

Consultations de la notice

885

Téléchargements de fichiers

213