کد مقاله کد نشریه سال انتشار مقاله انگلیسی نسخه تمام متن
436347 689993 2008 15 صفحه PDF دانلود رایگان
عنوان انگلیسی مقاله ISI
Characterizing strong normalization in the Curien–Herbelin symmetric lambda calculus: Extending the Coppo–Dezani heritage
موضوعات مرتبط
مهندسی و علوم پایه مهندسی کامپیوتر نظریه محاسباتی و ریاضیات
پیش نمایش صفحه اول مقاله
Characterizing strong normalization in the Curien–Herbelin symmetric lambda calculus: Extending the Coppo–Dezani heritage
چکیده انگلیسی

We develop an intersection type system for the  calculus of Curien and Herbelin. This calculus provides a symmetric computational interpretation of classical sequent style logic and gives a simple account of call-by-name and call-by-value. The present system improves upon earlier type disciplines for : in addition to characterizing the  expressions that are strongly normalizing under free (unrestricted) reduction, the system enjoys the Subject Reduction and the Subject Expansion properties.

ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Theoretical Computer Science - Volume 398, Issues 1–3, 28 May 2008, Pages 114-128