An Output-Based Semantics of Λμ with Explicit Substitution in the π-Calculus - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2012

An Output-Based Semantics of Λμ with Explicit Substitution in the π-Calculus

Steffen Van Bakel
  • Fonction : Auteur
  • PersonId : 1011790
Maria Grazia Vigliotti
  • Fonction : Auteur
  • PersonId : 1011791

Résumé

We study the Λμ-calculus, extended with explicit substitution, and define a compositional output-based translation into a variant of the π-calculus with pairing. We show that this translation preserves single-step explicit head reduction with respect to contextual equivalence. We use this result to show operational soundness for head reduction, adequacy, and operational completeness. Using a notion of implicative type-context assignment for the π-calculus, we also show that assignable types are preserved by the translation. We finish by showing that termination is preserved.
Fichier principal
Vignette du fichier
978-3-642-33475-7_26_Chapter.pdf (201.16 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-01556215 , version 1 (04-07-2017)

Licence

Paternité

Identifiants

Citer

Steffen Van Bakel, Maria Grazia Vigliotti. An Output-Based Semantics of Λμ with Explicit Substitution in the π-Calculus. 7th International Conference on Theoretical Computer Science (TCS), Sep 2012, Amsterdam, Netherlands. pp.372-387, ⟨10.1007/978-3-642-33475-7_26⟩. ⟨hal-01556215⟩
101 Consultations
42 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More