A fully-abstract semantics of lambda-mu in the pi-calculus
| Autor: | Maria Grazia Vigliotti, Steffen van Bakel |
|---|---|
| Jazyk: | angličtina |
| Rok vydání: | 2014 |
| Předmět: |
FOS: Computer and information sciences
Computer Science - Logic in Computer Science Pure mathematics Reduction (recursion theory) Semantics (computer science) lcsh:Mathematics Lambda lcsh:QA1-939 Weak equivalence lcsh:QA75.5-76.95 Logic in Computer Science (cs.LO) Interpretation (model theory) Abstraction (mathematics) Explicit substitution Pairing F.3.2 lcsh:Electronic computers. Computer science Mathematics |
| Zdroj: | Electronic Proceedings in Theoretical Computer Science, Vol 164, Iss Proc. CL&C 2014, Pp 33-47 (2014) CL&C |
| ISSN: | 2075-2180 |
| Popis: | We study the lambda-mu-calculus, extended with explicit substitution, and define a compositional output-based interpretation into a variant of the pi-calculus with pairing that preserves single-step explicit head reduction with respect to weak bisimilarity. We define four notions of weak equivalence for lambda-mu -- one based on weak reduction, two modelling weak head-reduction and weak explicit head reduction (all considering terms without weak head-normal form equivalent as well), and one based on weak approximation -- and show they all coincide. We will then show full abstraction results for our interpretation for the weak equivalences with respect to weak bisimilarity on processes. Comment: In Proceedings CL&C 2014, arXiv:1409.2593 |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|