%0 Conference Proceedings
%T An Output-Based Semantics of Λμ with Explicit Substitution in the π-Calculus
%+ Imperial College London
%A Bakel, Steffen, Van
%A Vigliotti, Maria, Grazia
%< avec comité de lecture
%( Lecture Notes in Computer Science
%B 7th International Conference on Theoretical Computer Science (TCS)
%C Amsterdam, Netherlands
%Y Jos C. M. Baeten
%Y Tom Ball
%Y Frank S. Boer
%I Springer
%3 Theoretical Computer Science
%V LNCS-7604
%P 372-387
%8 2012-09-26
%D 2012
%R 10.1007/978-3-642-33475-7_26
%Z Computer Science [cs]Conference papers
%X 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.
%G English
%Z TC 1
%Z TC 2
%Z WG 2.2
%2 https://inria.hal.science/hal-01556215/document
%2 https://inria.hal.science/hal-01556215/file/978-3-642-33475-7_26_Chapter.pdf
%L hal-01556215
%U https://inria.hal.science/hal-01556215
%~ IFIP-LNCS
%~ IFIP
%~ IFIP-TC
%~ IFIP-TC1
%~ IFIP-TC2
%~ IFIP-TCS
%~ IFIP-WG2-2
%~ IFIP-LNCS-7604