Bounding normalization time through intersection types
نشر في EPTCS
بتاريخ 2013
في مجال الهندسة المعلوماتية
والبحث باللغة
English
تحميل البحث
الملخص بالإنكليزية
Non-idempotent intersection types are used in order to give a bound of the length of the normalization beta-reduction sequence of a lambda term: namely, the bound is expressed as a function of the size of the term.