Skip to Main content Skip to Navigation
Reports

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

https://hal.inria.fr/inria-00074263
Contributor : Rapport de Recherche Inria <>
Submitted on : Wednesday, May 24, 2006 - 2:53:43 PM
Last modification on : Thursday, February 11, 2021 - 2:48:31 PM
Long-term archiving on: : Monday, April 5, 2010 - 12:07:28 AM

Identifiers

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

Share

Metrics

Record views

916

Files downloads

315