Observational Equivalence for the Interaction Combinators and Internal Separation

Damiano Mazza

doi:10.1016/j.entcs.2006.10.030

Observational Equivalence for the Interaction Combinators and Internal Separation

Damiano Mazza

Université de Provence

Résultats de recherche: Contribution à un journal › Article › Revue par des pairs

1 Citation (Scopus)

Résumé

We define an observational equivalence for Lafont's interaction combinators, which we prove to be the least discriminating non-trivial congruence on total nets (nets admitting a deadlock-free normal form) respecting reduction. More interestingly, this equivalence enjoys an internal separation property similar to that of Böhm's Theorem for the λ-calculus.

langue originale	Anglais
Pages (de - à)	113-137
Nombre de pages	25
journal	Electronic Notes in Theoretical Computer Science
Volume	176
Numéro de publication	1
Les DOIs	https://doi.org/10.1016/j.entcs.2006.10.030
état	Publié - 28 mai 2007
Modification externe	Oui

Accès au document

10.1016/j.entcs.2006.10.030

Contient cette citation

@article{f46e10e66a7b4694843207f629a98bcf,

title = "Observational Equivalence for the Interaction Combinators and Internal Separation",

abstract = "We define an observational equivalence for Lafont's interaction combinators, which we prove to be the least discriminating non-trivial congruence on total nets (nets admitting a deadlock-free normal form) respecting reduction. More interestingly, this equivalence enjoys an internal separation property similar to that of B{\"o}hm's Theorem for the λ-calculus.",

keywords = "B{\"o}hm's Theorem, Interaction nets, interaction combinators, internal separation, observational equivalence",

author = "Damiano Mazza",

year = "2007",

month = may,

day = "28",

doi = "10.1016/j.entcs.2006.10.030",

language = "English",

volume = "176",

pages = "113--137",

journal = "Electronic Notes in Theoretical Computer Science",

issn = "1571-0661",

publisher = "Elsevier B.V.",

number = "1",

}

TY - JOUR

T1 - Observational Equivalence for the Interaction Combinators and Internal Separation

AU - Mazza, Damiano

PY - 2007/5/28

Y1 - 2007/5/28

N2 - We define an observational equivalence for Lafont's interaction combinators, which we prove to be the least discriminating non-trivial congruence on total nets (nets admitting a deadlock-free normal form) respecting reduction. More interestingly, this equivalence enjoys an internal separation property similar to that of Böhm's Theorem for the λ-calculus.

AB - We define an observational equivalence for Lafont's interaction combinators, which we prove to be the least discriminating non-trivial congruence on total nets (nets admitting a deadlock-free normal form) respecting reduction. More interestingly, this equivalence enjoys an internal separation property similar to that of Böhm's Theorem for the λ-calculus.

KW - Böhm's Theorem

KW - Interaction nets

KW - interaction combinators

KW - internal separation

KW - observational equivalence

U2 - 10.1016/j.entcs.2006.10.030

DO - 10.1016/j.entcs.2006.10.030

M3 - Article

AN - SCOPUS:34248530867

SN - 1571-0661

VL - 176

SP - 113

EP - 137

JO - Electronic Notes in Theoretical Computer Science

JF - Electronic Notes in Theoretical Computer Science

IS - 1

ER -

Observational Equivalence for the Interaction Combinators and Internal Separation

Résumé

Accès au document

Empreinte digitale

Contient cette citation