Proof nets and the call-by-value lambda-calculus
This paper gives a detailed account of the relationship between (a variant of) the call-by-value lambda calculus and linear logic proof nets. The presentation is carefully tuned in order to realize a strong bisimulation between the two systems: every single rewriting step on the calculus maps to a s...
| Main Author: | |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Open Publishing Association
2013-03-01
|
| Series: | Electronic Proceedings in Theoretical Computer Science |
| Online Access: | http://arxiv.org/pdf/1303.7326v1 |
| _version_ | 1811294014955061248 |
|---|---|
| author | Beniamino Accattoli |
| author_facet | Beniamino Accattoli |
| author_sort | Beniamino Accattoli |
| collection | DOAJ |
| description | This paper gives a detailed account of the relationship between (a variant of) the call-by-value lambda calculus and linear logic proof nets. The presentation is carefully tuned in order to realize a strong bisimulation between the two systems: every single rewriting step on the calculus maps to a single step on the nets, and viceversa. In this way, we obtain an algebraic reformulation of proof nets. Moreover, we provide a simple correctness criterion for our proof nets, which employ boxes in an unusual way. |
| first_indexed | 2024-04-13T05:10:54Z |
| format | Article |
| id | doaj.art-7404f2918a744a108c370ad8ff8cea39 |
| institution | Directory Open Access Journal |
| issn | 2075-2180 |
| language | English |
| last_indexed | 2024-04-13T05:10:54Z |
| publishDate | 2013-03-01 |
| publisher | Open Publishing Association |
| record_format | Article |
| series | Electronic Proceedings in Theoretical Computer Science |
| spelling | doaj.art-7404f2918a744a108c370ad8ff8cea392022-12-22T03:01:02ZengOpen Publishing AssociationElectronic Proceedings in Theoretical Computer Science2075-21802013-03-01113Proc. LSFA 2012112610.4204/EPTCS.113.5Proof nets and the call-by-value lambda-calculusBeniamino AccattoliThis paper gives a detailed account of the relationship between (a variant of) the call-by-value lambda calculus and linear logic proof nets. The presentation is carefully tuned in order to realize a strong bisimulation between the two systems: every single rewriting step on the calculus maps to a single step on the nets, and viceversa. In this way, we obtain an algebraic reformulation of proof nets. Moreover, we provide a simple correctness criterion for our proof nets, which employ boxes in an unusual way.http://arxiv.org/pdf/1303.7326v1 |
| spellingShingle | Beniamino Accattoli Proof nets and the call-by-value lambda-calculus Electronic Proceedings in Theoretical Computer Science |
| title | Proof nets and the call-by-value lambda-calculus |
| title_full | Proof nets and the call-by-value lambda-calculus |
| title_fullStr | Proof nets and the call-by-value lambda-calculus |
| title_full_unstemmed | Proof nets and the call-by-value lambda-calculus |
| title_short | Proof nets and the call-by-value lambda-calculus |
| title_sort | proof nets and the call by value lambda calculus |
| url | http://arxiv.org/pdf/1303.7326v1 |
| work_keys_str_mv | AT beniaminoaccattoli proofnetsandthecallbyvaluelambdacalculus |