HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
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 metadata

Cited literature [56 references]  Display  Hide  Download

https://hal.inria.fr/hal-02536463
Contributor : Sergueï Lenglet Connect in order to contact the contributor
Submitted on : Friday, September 4, 2020 - 11:09:24 AM
Last modification on : Monday, April 4, 2022 - 9:28:24 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

205

Files downloads

380