کد مقاله | کد نشریه | سال انتشار | مقاله انگلیسی | نسخه تمام متن |
---|---|---|---|---|
435776 | 689935 | 2015 | 23 صفحه PDF | دانلود رایگان |
عنوان انگلیسی مقاله ISI
Proof nets and the call-by-value λ-calculus
دانلود مقاله + سفارش ترجمه
دانلود مقاله ISI انگلیسی
رایگان برای ایرانیان
کلمات کلیدی
موضوعات مرتبط
مهندسی و علوم پایه
مهندسی کامپیوتر
نظریه محاسباتی و ریاضیات
پیش نمایش صفحه اول مقاله
![عکس صفحه اول مقاله: Proof nets and the call-by-value λ-calculus Proof nets and the call-by-value λ-calculus](/preview/png/435776.png)
چکیده انگلیسی
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 an isomorphism between the two systems: every single rewriting step on the calculus maps to a single step on proof nets, and vice-versa. 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, and identify a subcalculus that is shown to be as expressive as the full calculus.
ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Theoretical Computer Science - Volume 606, 16 November 2015, Pages 2–24
Journal: Theoretical Computer Science - Volume 606, 16 November 2015, Pages 2–24
نویسندگان
Beniamino Accattoli,