Trees from Functions as Processes
Levy-Longo Trees and Bohm Trees are the best known tree structures on the {\lambda}-calculus. We give general conditions under which an encoding of the {\lambda}-calculus into the {\pi}-calculus is sound and complete with respect to such trees. We apply these conditions to various encodings of the c...
| Main Authors: | , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Logical Methods in Computer Science e.V.
2018-08-01
|
| Series: | Logical Methods in Computer Science |
| Subjects: | |
| Online Access: | https://lmcs.episciences.org/4448/pdf |
| _version_ | 1797268603338227712 |
|---|---|
| author | Davide Sangiorgi Xian Xu |
| author_facet | Davide Sangiorgi Xian Xu |
| author_sort | Davide Sangiorgi |
| collection | DOAJ |
| description | Levy-Longo Trees and Bohm Trees are the best known tree structures on the
{\lambda}-calculus. We give general conditions under which an encoding of the
{\lambda}-calculus into the {\pi}-calculus is sound and complete with respect
to such trees. We apply these conditions to various encodings of the
call-by-name {\lambda}-calculus, showing how the two kinds of tree can be
obtained by varying the behavioural equivalence adopted in the {\pi}-calculus
and/or the encoding. |
| first_indexed | 2024-04-25T01:35:06Z |
| format | Article |
| id | doaj.art-fc6cde96d9514e21ac25758e660dc002 |
| institution | Directory Open Access Journal |
| issn | 1860-5974 |
| language | English |
| last_indexed | 2024-04-25T01:35:06Z |
| publishDate | 2018-08-01 |
| publisher | Logical Methods in Computer Science e.V. |
| record_format | Article |
| series | Logical Methods in Computer Science |
| spelling | doaj.art-fc6cde96d9514e21ac25758e660dc0022024-03-08T10:02:03ZengLogical Methods in Computer Science e.V.Logical Methods in Computer Science1860-59742018-08-01Volume 14, Issue 310.23638/LMCS-14(3:11)20184448Trees from Functions as ProcessesDavide SangiorgiXian XuLevy-Longo Trees and Bohm Trees are the best known tree structures on the {\lambda}-calculus. We give general conditions under which an encoding of the {\lambda}-calculus into the {\pi}-calculus is sound and complete with respect to such trees. We apply these conditions to various encodings of the call-by-name {\lambda}-calculus, showing how the two kinds of tree can be obtained by varying the behavioural equivalence adopted in the {\pi}-calculus and/or the encoding.https://lmcs.episciences.org/4448/pdfcomputer science - logic in computer science |
| spellingShingle | Davide Sangiorgi Xian Xu Trees from Functions as Processes Logical Methods in Computer Science computer science - logic in computer science |
| title | Trees from Functions as Processes |
| title_full | Trees from Functions as Processes |
| title_fullStr | Trees from Functions as Processes |
| title_full_unstemmed | Trees from Functions as Processes |
| title_short | Trees from Functions as Processes |
| title_sort | trees from functions as processes |
| topic | computer science - logic in computer science |
| url | https://lmcs.episciences.org/4448/pdf |
| work_keys_str_mv | AT davidesangiorgi treesfromfunctionsasprocesses AT xianxu treesfromfunctionsasprocesses |