HOπ in Coq

Sergueï Lenglet (1) , Alan Schmitt (2)

1 MOSEL - Proof-oriented development of computer-based systems
2 CELTIQUE - Software certification with semantic analysis

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.

Mots clés: CCS Concepts • Theory of computation → Process calculi; Coq formalization; Higher-order process calculus; Howe’s method

Domaines: Théorie et langage formel [cs.FL]

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⟩