کد مقاله | کد نشریه | سال انتشار | مقاله انگلیسی | نسخه تمام متن |
---|---|---|---|---|
424080 | 685333 | 2007 | 17 صفحه PDF | دانلود رایگان |
عنوان انگلیسی مقاله ISI
A Formalization of Strong Normalization for Simply-Typed Lambda-Calculus and System F
دانلود مقاله + سفارش ترجمه
دانلود مقاله ISI انگلیسی
رایگان برای ایرانیان
موضوعات مرتبط
مهندسی و علوم پایه
مهندسی کامپیوتر
نظریه محاسباتی و ریاضیات
پیش نمایش صفحه اول مقاله

چکیده انگلیسی
We formalize in the logical framework ATS/LF a proof based on Tait's method that establishes the simply-typed lambda-calculus being strongly normalizing. In this formalization, we employ higher-order abstract syntax to encode lambda-terms and an inductive datatype to encode the reducibility predicate in Tait's method. The resulting proof is particularly simple and clean when compared to previously formalized ones. Also, we mention briefly how a proof based on Girard's method can be formalized in a similar fashion that establishes System F being strongly normalizing.
ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Electronic Notes in Theoretical Computer Science - Volume 174, Issue 5, 2 June 2007, Pages 109-125
Journal: Electronic Notes in Theoretical Computer Science - Volume 174, Issue 5, 2 June 2007, Pages 109-125