First-Order Reasoning for Higher-Order Concurrency.
File Type:
PDFItem Type:
Journal ArticleDate:
2012Access:
OpenAccessCitation:
Vasileios Koutavas and Matthew Hennessy, First-Order Reasoning for Higher-Order Concurrency., Journal of Computer Languages, Systems and Structures, 38, 3, 2012, 242-277Download Item:
hopi-comlan-preprint.pdf (Published (author's copy) - Peer Reviewed) 305.3Kb
Abstract:
We present a practical first-order theory of a higher-order pi-calculus which is both sound and complete with respect to a standard semantic equivalence. The theory is a product of combining and simplifying two of the most prominent theories for HOpi of Sangiorgi et al. and Jeffrey and Rathke [10, 21], and a novel approach to scope extrusion. In this way we obtain an elementary labelled transition system where the standard theory of first-order weak bisimulation and its corresponding propositional Hennessy?Milner logic can be applied.
The usefulness of our theory is demonstrated by straightforward proofs of equivalences between compact but intricate higher-order processes using witness first-order bisimulations, and proofs of inequivalence using the propositional Hennessy?Milner logic. Finally we show that contextual equivalence in a higher-order setting is a conservative extension of the first-order pi-calculus.
Sponsor
Grant Number
Science Foundation Ireland (SFI)
06 IN.1 1898.
Author's Homepage:
http://people.tcd.ie/mcbhennehttp://people.tcd.ie/vkoutav
Description:
PUBLISHED
Author: HENNESSY, MATTHEW; KOUTAVAS, VASILEIOS
Type of material:
Journal ArticleCollections:
Series/Report no:
Journal of Computer Languages, Systems and Structures38
3
Availability:
Full text availableKeywords:
concurrencyDOI:
http://dx.doi.org/10.1016/j.cl.2012.04.003Licences: