HOπ in Coq

Sergueï Lenglet 1 Alan Schmitt 2
1 VERIDIS - Modeling and Verification of Distributed Algorithms and Systems
Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
2 CELTIQUE - Software certification with semantic analysis
Inria Rennes – Bretagne Atlantique , IRISA_D4 - LANGAGE ET GÉNIE LOGICIEL
Abstract : We propose a formalization in Coq of HOπ , a process calculus where messages carry processes. Such a higher-order calculus features two very different kinds of binder: process input, similar to λ-abstraction, and name restriction, whose scope can be expanded by communication. We formalize strong context bisimilarity and prove it is compatible using Howe's method, based on several proof schemes we developed in a previous paper.
Type de document :
Communication dans un congrès
CPP 2018 - The 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, Jan 2018, Los Angeles, United States. pp.14, 2018, 〈10.1145/3167083〉
Liste complète des métadonnées

Littérature citée [23 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01614987
Contributeur : Sergueï Lenglet <>
Soumis le : vendredi 15 décembre 2017 - 15:06:46
Dernière modification le : mercredi 26 septembre 2018 - 01:12:53

Fichier

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

Identifiants

Citation

Sergueï Lenglet, Alan Schmitt. HOπ in Coq. CPP 2018 - The 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, Jan 2018, Los Angeles, United States. pp.14, 2018, 〈10.1145/3167083〉. 〈hal-01614987v3〉

Partager

Métriques

Consultations de la notice

587

Téléchargements de fichiers

114