کد مقاله | کد نشریه | سال انتشار | مقاله انگلیسی | نسخه تمام متن |
---|---|---|---|---|
426490 | 686082 | 2014 | 16 صفحه PDF | دانلود رایگان |
عنوان انگلیسی مقاله ISI
Krivine machines and higher-order schemes
ترجمه فارسی عنوان
ماشین آلات کریوین و طرح های مرتبه بالاتر یک
دانلود مقاله + سفارش ترجمه
دانلود مقاله ISI انگلیسی
رایگان برای ایرانیان
موضوعات مرتبط
مهندسی و علوم پایه
مهندسی کامپیوتر
نظریه محاسباتی و ریاضیات
چکیده انگلیسی
We propose a new approach to analyzing higher-order recursive schemes. Many results in the literature use automata models generalizing pushdown automata, most notably higher-order pushdown automata with collapse (CPDA). Instead, we propose to use the Krivine machine model. Compared to CPDA, this model is closer to lambda-calculus, and incorporates nicely many invariants of computations, as for example the typing information. The usefulness of the proposed approach is demonstrated with new proofs of two central results in the field: the decidability of the local and global model checking problems for higher-order schemes with respect to the mu-calculus.
ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Information and Computation - Volume 239, December 2014, Pages 340–355
Journal: Information and Computation - Volume 239, December 2014, Pages 340–355
نویسندگان
Sylvain Salvati, Igor Walukiewicz,