HOπ in Coq

Sergueï Lenglet 1 Alan Schmitt 2
1 VERIDIS - Modeling and Verification of Distributed Algorithms and Systems
LORIA - FM - Department of Formal Methods , Inria Nancy - Grand Est, MPII - Max-Planck-Institut für Informatik
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.
Document type :
Conference papers
Complete list of metadatas

Cited literature [23 references]  Display  Hide  Download

Contributor : Sergueï Lenglet <>
Submitted on : Friday, December 15, 2017 - 3:06:46 PM
Last modification on : Friday, September 13, 2019 - 9:48:42 AM


Files produced by the author(s)



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, ⟨10.1145/3167083⟩. ⟨hal-01614987v3⟩



Record views


Files downloads