کد مقاله | کد نشریه | سال انتشار | مقاله انگلیسی | نسخه تمام متن |
---|---|---|---|---|
422263 | 685057 | 2016 | 17 صفحه PDF | دانلود رایگان |
عنوان انگلیسی مقاله ISI
Strong Normalization through Intersection Types and Memory
ترجمه فارسی عنوان
عادی سازی قدرتمند ازطریق انواع تقاطع و حافظه
دانلود مقاله + سفارش ترجمه
دانلود مقاله ISI انگلیسی
رایگان برای ایرانیان
کلمات کلیدی
حساب لامبدا ؛ حساب حافظه؛ عادی سازی قدرتمند ؛ انواع تقاطع
موضوعات مرتبط
مهندسی و علوم پایه
مهندسی کامپیوتر
نظریه محاسباتی و ریاضیات
چکیده انگلیسی
We characterize β-strongly normalizing λ-terms by means of a non-idempotent intersection type system. More precisely, we first define a memory calculus K together with a non-idempotent intersection type system K, and we show that a K-term t is typable in KK if and only if t is K-strongly normalizing. We then show that β-strong normalization is equivalent to K-strong normalization. We conclude since λ-terms are strictly included in K-terms.
ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Electronic Notes in Theoretical Computer Science - Volume 323, 11 July 2016, Pages 75–91
Journal: Electronic Notes in Theoretical Computer Science - Volume 323, 11 July 2016, Pages 75–91
نویسندگان
Antonio Bucciarelli, Delia Kesner, Daniel Ventura,