Reseña: HOCore in Coq
Se ha publicado un artículo de razonamiento formalizado en Coq titulado HOCore in Coq.
Sus autores son
- Martín Escarrá(de la Universidad Nacional de Rosario, Argentina),
- Maksimović Petar (del grupo Celtique en el INRIA Rennes) y
- Alan Schmitt (del grupo Celtique en el INRIA Rennes)
Su resumen es
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.
El trabajo se ha presentado en las Journées Francophones des Langages Applicatifs (JFLA 2015).
El código de las correspondientes teorías en Coq se encuentra aquí.