Skip to Main content Skip to Navigation
Conference papers

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

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.
Document type :
Conference papers
Complete list of metadata

Cited literature [30 references]  Display  Hide  Download

https://hal.inria.fr/hal-01556215
Contributor : Hal Ifip <>
Submitted on : Tuesday, July 4, 2017 - 5:45:39 PM
Last modification on : Tuesday, July 4, 2017 - 5:47:02 PM
Long-term archiving on: : Friday, December 15, 2017 - 1:32:22 AM

File

978-3-642-33475-7_26_Chapter.p...
Files produced by the author(s)

Licence


Distributed under a Creative Commons Attribution 4.0 International License

Identifiers

Citation

Steffen Bakel, Maria 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⟩

Share

Metrics

Record views

150

Files downloads

154