HOπ in Coq - Archive ouverte HAL Access content directly
Conference Papers Year : 2018

HOπ in Coq

(1) , (2)
1
2

Abstract

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.
Fichier principal
Vignette du fichier
cpp18.pdf (696.44 Ko) Télécharger le fichier
Origin : Files produced by the author(s)
Loading...

Dates and versions

hal-01614987 , version 1 (11-10-2017)
hal-01614987 , version 2 (28-11-2017)
hal-01614987 , version 3 (15-12-2017)

Identifiers

Cite

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⟩
1087 View
552 Download

Altmetric

Share

Gmail Facebook Twitter LinkedIn More