کد مقاله کد نشریه سال انتشار مقاله انگلیسی نسخه تمام متن
422263 685057 2016 17 صفحه PDF دانلود رایگان
عنوان انگلیسی مقاله ISI
Strong Normalization through Intersection Types and Memory
ترجمه فارسی عنوان
عادی سازی قدرتمند ازطریق انواع تقاطع و حافظه
کلمات کلیدی
حساب لامبدا ؛ حساب حافظه؛ عادی سازی قدرتمند ؛ انواع تقاطع
موضوعات مرتبط
مهندسی و علوم پایه مهندسی کامپیوتر نظریه محاسباتی و ریاضیات
چکیده انگلیسی

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
نویسندگان
, , ,