Abstract : 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.
Type de document :
Communication dans un congrès
Jos C. M. Baeten; Tom Ball; Frank S. Boer. 7th International Conference on Theoretical Computer Science (TCS), Sep 2012, Amsterdam, Netherlands. Springer, Lecture Notes in Computer Science, LNCS-7604, pp.372-387, 2012, Theoretical Computer Science. 〈10.1007/978-3-642-33475-7_26〉
https://hal.inria.fr/hal-01556215
Contributeur : Hal Ifip
<>
Soumis le : mardi 4 juillet 2017 - 17:45:39
Dernière modification le : mardi 4 juillet 2017 - 17:47:02
Document(s) archivé(s) le : vendredi 15 décembre 2017 - 01:32:22
Steffen Bakel, Maria Vigliotti. An Output-Based Semantics of Λμ with Explicit Substitution in the π-Calculus. Jos C. M. Baeten; Tom Ball; Frank S. Boer. 7th International Conference on Theoretical Computer Science (TCS), Sep 2012, Amsterdam, Netherlands. Springer, Lecture Notes in Computer Science, LNCS-7604, pp.372-387, 2012, Theoretical Computer Science. 〈10.1007/978-3-642-33475-7_26〉. 〈hal-01556215〉
