کد مقاله کد نشریه سال انتشار مقاله انگلیسی نسخه تمام متن
426920 686355 2007 16 صفحه PDF دانلود رایگان
عنوان انگلیسی مقاله ISI
Intersection-types à la Church
موضوعات مرتبط
مهندسی و علوم پایه مهندسی کامپیوتر نظریه محاسباتی و ریاضیات
پیش نمایش صفحه اول مقاله
Intersection-types à la Church
چکیده انگلیسی

In this paper, we present , a fully typed λ-calculus based on the intersection-type system discipline, which is a counterpart à la Church of the type assignment system as invented by Coppo and Dezani. The relationship between and the intersection type assignment system is the standard isomorphism between typed and type assignment system, and so the typed language inherits from the untyped system all the good properties, like subject reduction and strong normalization. Moreover, both type checking and type reconstruction are decidable.

ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Information and Computation - Volume 205, Issue 9, September 2007, Pages 1371-1386