Formalisation de HOCore en CoqReportar como inadecuado




Formalisation de HOCore en Coq - Descarga este documento en PDF. Documentación en PDF para descargar gratis. Disponible también para leer online.

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.





Autor: Simon Boulier - Alan Schmitt -

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



DESCARGAR PDF




Documentos relacionados