Skip to Main content Skip to Navigation
New interface
Conference papers

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

Cited literature [27 references]  Display  Hide  Download
Contributor : David Baelde Connect in order to contact the contributor
Submitted on : Wednesday, December 31, 2014 - 3:30:25 PM
Last modification on : Wednesday, February 2, 2022 - 3:50:45 PM
Long-term archiving on: : Saturday, April 15, 2017 - 12:20:16 PM


Files produced by the author(s)


  • HAL Id : hal-01099130, version 1


Martín Escarrá, Petar Maksimović, Alan Schmitt. HOCore in Coq. Vingt-sixièmes Journées Francophones des Langages Applicatifs (JFLA 2015), Jan 2015, Le Val d'Ajol, France. ⟨hal-01099130⟩



Record views


Files downloads