HOπ in Coq

Guillaume Ambal (1, 2) , Sergueï Lenglet (3) , Alan Schmitt (1)

1 CELTIQUE - Software certification with semantic analysis
2 ENS de Lyon - École normale supérieure de Lyon
3 MOSEL - Proof-oriented development of computer-based systems

We present a formalization of HOπ in Coq, 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. For the latter, we compare four approaches to represent binders: locally nameless, de Bruijn indices, nominal, and Higher-Order Abstract Syntax. In each case, we formalize strong context bisimi-larity and prove it is compatible, i.e., closed under every context, using Howe's method, based on several proof schemes we developed in a previous paper.

Mots clés: Coq; Higher-order process calculus; Howe's method

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

Guillaume Ambal, Sergueï Lenglet, Alan Schmitt. HOπ in Coq. Journal of Automated Reasoning, 2020, ⟨10.1007/s10817-020-09553-0⟩. ⟨hal-02536463v2⟩