HOπ in Coq - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Article Dans Une Revue Journal of Automated Reasoning Année : 2020

HOπ in Coq

Résumé

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.
Fichier principal
Vignette du fichier
jar-depyg.pdf (596.56 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-02536463 , version 1 (08-04-2020)
hal-02536463 , version 2 (04-09-2020)

Identifiants

Citer

Guillaume Ambal, Sergueï Lenglet, Alan Schmitt. HOπ in Coq. Journal of Automated Reasoning, In press, ⟨10.1145/3167083⟩. ⟨hal-02536463v1⟩
294 Consultations
496 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More