Characterizing contextual equivalence in calculi with passivation

Sergueï Lenglet 1 Alan Schmitt 1 Jean-Bernard Stefani 1, *
* Auteur correspondant
1 SARDES - System architecture for reflective distributed computing environments
Inria Grenoble - Rhône-Alpes, LIG - Laboratoire d'Informatique de Grenoble
Abstract : We study the problem of characterizing contextual equivalence in higher-order languages with passivation. To overcome the difficulties arising in the proof of congruence of candidate bisimilarities, we introduce a new form of labeled 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 the presence of an early form of bisimulation. We use complementary semantics to provide a coinductive characterization of contextual equivalence in the HOπP calculus, an extension of the higher-order π-calculus with passivation, obtaining the first result of this kind. We then study the problem of defining a more effective variant of bisimilarity that still characterizes contextual equivalence, along the lines of Sangiorgiʼs notion of normal bisimilarity. We provide partial results on this difficult 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 defined for HOπP without restriction.
Type de document :
Article dans une revue
Information and Computation, Elsevier, 2011, 209 (11), pp.1390-1433. 〈10.1016/j.ic.2011.08.002〉
Liste complète des métadonnées

Littérature citée [42 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-00903877
Contributeur : Sergueï Lenglet <>
Soumis le : mercredi 13 novembre 2013 - 12:02:21
Dernière modification le : mercredi 11 avril 2018 - 01:52:56
Document(s) archivé(s) le : vendredi 14 février 2014 - 15:45:12

Fichier

journal.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Sergueï Lenglet, Alan Schmitt, Jean-Bernard Stefani. Characterizing contextual equivalence in calculi with passivation. Information and Computation, Elsevier, 2011, 209 (11), pp.1390-1433. 〈10.1016/j.ic.2011.08.002〉. 〈hal-00903877〉

Partager

Métriques

Consultations de la notice

2652

Téléchargements de fichiers

146