Author | Conference | Journal | Organization | Year | DOI
Look for results that meet for the following criteria:
Academic
Publications
Characterizing Contextual Equivalence in Calculi with Passivation
Edit
Characterizing Contextual Equivalence in Calculi with Passivation   (Citations: 1)
BibTex | RIS | RefWorks Download
Abstract We study the problem of characterizing contextual equivalence in higher-order languages with passivation. To overcome the diculties,arising in the proof of congruence of candidate bisimilarities, we introduce a new form of labelled transition semantics together with its associated notion of bisimulation, which we call complementary semantics. Complementary semantics allows to apply the well-known Howe’s method,for proving the congruence of bisimilarities in a higher-order setting, even in presence of an early form of bisimulation. We use complementary semantics to provide a coinductive characterization of con- textual equivalence in the HO P calculus, an extension of the higher-order - calculus with passivation, obtaining the rst result of this kind. We then study the problem of dening,a more eective,variant of bisimilarity that still char- acterizes contextual equivalence, along the lines of Sangiorgi’s notion of normal bisimilarity. We provide partial results on this dicult,problem: we show that a large class of test processes cannot be used to derive a normal bisimilarity in HO P, but we show that a form of normal bisimilarity can be dened for HO P without restriction.
Published in 2010.
Cumulative Annual
View Publication
The following links allow you to view full publications. These links are maintained by other sources not affiliated with Microsoft Academic Search.
    • ...Proofs and additional details are available in the draft of the full paper [14]...
    • ...Scope extrusion outside localities is performed \by need" when a communication takes place, as dened in the extension of restriction to concretions in Fig. 1. Note that with this semantics, the interaction between passivation and restriction is not benign: in general processes b[a:P ] and a:b [P ] are not barbed congruent (see [14] for more details)...
    • ...The proof of congruence in Theorem 1 is the same as in the Kell calculus [24] (see [14] for details)...
    • ...Communication problem. To prove thatR is a simulation, we need to establish a stronger result, to avoid transitivity issues which otherwise would arise and make the method fail in the weak case [14]...

    Sergueï Lenglet, et al. Howe's Method for Calculi with Passivation

Order by:

Citations (1)

Share this on | Contribute to Academic