HOCore in Coq

Martín Escarrá 1 Petar Maksimović 2 Alan Schmitt 2
2 CELTIQUE - Software certification with semantic analysis
Inria Rennes – Bretagne Atlantique , IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL
Abstract : We consider a recent publication on higher-order process calculi and describe how its results are formalized in the Coq proof assistant. We also highlight some important technical issues that we have uncovered in the original publication. We believe these issues are not unique to the paper under consideration, and require particular care to be avoided. Our ultimate goal is to show that it is possible to build a solid, high-confidence setting for formal reasoning on higher-order process calculi.
Type de document :
Communication dans un congrès
David Baelde; Jade Alglave. Vingt-sixièmes Journées Francophones des Langages Applicatifs (JFLA 2015), Jan 2015, Le Val d'Ajol, France. Actes des Vingt-sixièmes Journées Francophones des Langages Applicatifs (JFLA 2015), <http://jfla.inria.fr/2015>
Liste complète des métadonnées


https://hal.inria.fr/hal-01099130
Contributeur : David Baelde <>
Soumis le : mercredi 31 décembre 2014 - 15:30:25
Dernière modification le : vendredi 17 février 2017 - 16:11:23

Fichier

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

Identifiants

  • HAL Id : hal-01099130, version 1

Citation

Martín Escarrá, Petar Maksimović, Alan Schmitt. HOCore in Coq. David Baelde; Jade Alglave. Vingt-sixièmes Journées Francophones des Langages Applicatifs (JFLA 2015), Jan 2015, Le Val d'Ajol, France. Actes des Vingt-sixièmes Journées Francophones des Langages Applicatifs (JFLA 2015), <http://jfla.inria.fr/2015>. <hal-01099130>

Partager

Métriques

Consultations de
la notice

449

Téléchargements du document

142