کد مقاله | کد نشریه | سال انتشار | مقاله انگلیسی | نسخه تمام متن |
---|---|---|---|---|
10334095 | 690171 | 2011 | 19 صفحه PDF | دانلود رایگان |
عنوان انگلیسی مقاله ISI
Realizability models and implicit complexity
دانلود مقاله + سفارش ترجمه
دانلود مقاله ISI انگلیسی
رایگان برای ایرانیان
کلمات کلیدی
موضوعات مرتبط
مهندسی و علوم پایه
مهندسی کامپیوتر
نظریه محاسباتی و ریاضیات
پیش نمایش صفحه اول مقاله

چکیده انگلیسی
New, simple, proofs of soundness (every representable function lies in a given complexity class) for Elementary Affine Logic, LFPLÂ and Soft Affine Logic are presented. The proofs are obtained by instantiating a semantic framework previously introduced by the authors and based on an innovative modification of realizability. The proof is a notable simplification on the original already semantic proof of soundness for the above mentioned logical systems and programming languages. A new result made possible by the semantic framework is the addition of polymorphism and a modality to LFPL, thus allowing for an internal definition of inductive datatypes. The methodology presented proceeds by assigning both abstract resource bounds in the form of elements from a resource monoid and resource-bounded computations to proofs (respectively, programs).
ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Theoretical Computer Science - Volume 412, Issue 20, 29 April 2011, Pages 2029-2047
Journal: Theoretical Computer Science - Volume 412, Issue 20, 29 April 2011, Pages 2029-2047
نویسندگان
Ugo Dal Lago, Martin Hofmann,