Formalisation de HOCore en CoqReport as inadecuate




Formalisation de HOCore en Coq - Download this document for free, or read online. Document in PDF available to download.

1 ENS Cachan Bretagne - École normale supérieure - Cachan, antenne de Bretagne 2 CELTIQUE - Software certification with semantic analysis Inria Rennes – Bretagne Atlantique , IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL

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, 2092: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, 2092: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.





Author: Simon Boulier - Alan Schmitt -

Source: https://hal.archives-ouvertes.fr/



DOWNLOAD PDF




Related documents