HOπ in Coq

Sergueï Lenglet 1 Alan Schmitt 2
2 CELTIQUE - Software certification with semantic analysis
Inria Rennes – Bretagne Atlantique , IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL
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.
Document type :
Preprints, Working Papers, ...
Complete list of metadatas

Cited literature [20 references]  Display  Hide  Download

https://hal.inria.fr/hal-01614987
Contributor : Sergueï Lenglet <>
Submitted on : Wednesday, October 11, 2017 - 4:57:38 PM
Last modification on : Friday, September 13, 2019 - 9:48:42 AM
Long-term archiving on : Friday, January 12, 2018 - 3:42:50 PM

File

cpp18.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01614987, version 1

Collections

Citation

Sergueï Lenglet, Alan Schmitt. HOπ in Coq. 2017. ⟨hal-01614987v1⟩

Share

Metrics

Record views

374

Files downloads

144