Skip to Main content Skip to Navigation
Journal articles

HOπ in Coq

Guillaume Ambal 1, 2 Sergueï Lenglet 3 Alan Schmitt 1
1 CELTIQUE - Software certification with semantic analysis
Inria Rennes – Bretagne Atlantique , IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL
3 MOSEL - Proof-oriented development of computer-based systems
LORIA - FM - Department of Formal Methods
Abstract : 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.
Document type :
Journal articles
Complete list of metadatas

Cited literature [56 references]  Display  Hide  Download

https://hal.inria.fr/hal-02536463
Contributor : Sergueï Lenglet <>
Submitted on : Friday, September 4, 2020 - 11:09:24 AM
Last modification on : Sunday, September 6, 2020 - 3:07:16 AM

File

jar.pdf
Files produced by the author(s)

Identifiers

Citation

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

Share

Metrics

Record views

28

Files downloads

57