Skip to Main content Skip to Navigation
Conference papers

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.
Document type :
Conference papers
Complete list of metadata

Cited literature [15 references]  Display  Hide  Download

https://hal.inria.fr/hal-00665945
Contributor : Alain Monteil <>
Submitted on : Friday, February 3, 2012 - 11:41:26 AM
Last modification on : Tuesday, June 15, 2021 - 4:30:25 PM
Long-term archiving on: : Wednesday, December 14, 2016 - 3:38:38 AM

File

paper_7.pdf
Files produced by the author(s)

Identifiers

  • 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. ⟨hal-00665945⟩

Share

Metrics

Record views

1470

Files downloads

253