Formalisation de HOCore en Coq

Résumé : Nous présentons les premiers résultats de la formalisation de propriétés du calcul de processus d'ordre supérieur HOCore [I. Lanese, J. A. Pérez, D. Sangiorgi et A. Schmitt : On the expressiveness and decidability of higher-order process calculi. Information and Computation, 209(2):198-226, fév. 2011.] dans l'assistant de preuve Coq. Nous décrivons notre choix de représentation des lieurs de HOCore, nous basant sur l'approche canonique de Pollack et al .[R. Pollack, M. Sato et W. Ricciotti : A canonical locally named representation of binding. Journal of Automated Reasoning, p. 1-23, mai 2011. 10.1007/s10817-011-9229-y.] Nous donnons la représentation de différentes notions de bissimulations, puis la preuve formelle de la correction de l'IO-bissimilarité par rapport à l'équivalence contextuelle barbue, correspondant à un des théorèmes fondamentaux de [I. Lanese, J. A. Pérez, D. Sangiorgi et A. Schmitt : On the expressiveness and decidability of higher-order process calculi. Information and Computation, 209(2):198-226, fév. 2011.]. Nous montrons également que l'IO-bissimilarité est décidable. L'objectif de ce travail est de montrer l'utilité de Coq et de la représentation canonique pour prouver des propriétés de calculs d'ordre supérieur.
Type de document :
Communication dans un congrès
JFLA - Journées Francophones des Langages Applicatifs - 2012, Feb 2012, Carnac, France. 2012
Liste complète des métadonnées

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

https://hal.inria.fr/hal-00665945
Contributeur : Alain Monteil <>
Soumis le : vendredi 3 février 2012 - 11:41:26
Dernière modification le : mercredi 16 mai 2018 - 11:23:28
Document(s) archivé(s) le : mercredi 14 décembre 2016 - 03:38:38

Fichier

paper_7.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-00665945, version 1

Citation

Simon Boulier, Alan Schmitt. Formalisation de HOCore en Coq. JFLA - Journées Francophones des Langages Applicatifs - 2012, Feb 2012, Carnac, France. 2012. 〈hal-00665945〉

Partager

Métriques

Consultations de la notice

971

Téléchargements de fichiers

194