-
a canonical locally named representation of binding
جزئیات بیشتر مقاله- تاریخ ارائه: 1392/07/24
- تاریخ انتشار در تی پی بین: 1392/07/24
- تعداد بازدید: 711
- تعداد پرسش و پاسخ ها: 0
- شماره تماس دبیرخانه رویداد: -
this paper is about completely formal representation of languages with binding. we have previously written about a representation following an approach going back to frege, based on first-order syntax using distinct syntactic classes for locally bound variables vs. global or free variables (sato and pollack, j symb comput 45:598–616, 2010). the present paper differs from our previous work by being more abstract. whereas we previously gave a particular concrete function for canonically choosing the names of binders, here we characterize abstractly the properties required of such a choice function to guarantee canonical representation, and focus on the metatheory of the representation, proving that it is in substitution preserving isomorphism with the nominal isabelle representation of pure lambda terms. this metatheory is formalized in isabelle/hol. the final section outlines a formalization in matita of a challenging language with multiple binding and simultaneous substitution. the isabelle and matita proof files are available online.
مقالات جدیدترین رویدادها
-
استفاده از تحلیل اهمیت-عملکرد در ارائه الگوی مدیریت خلاقیت سازمانی و ارائه راهکار جهت بهبود
-
بررسی تاثیر ارزش وجوه نقد مازاد بر ساختار سرمایه شرکت های پذیرفته شده در بورس اوراق بهادار تهران
-
بررسی تأثیر سطح افشای ریسک بر قرارداد بدهی شرکت های پذیرفته شده در بورس اوراق بهادار تهران
-
بررسی تأثیر رتبه بندی اعتباری مبتنی بر مدل امتیاز بازار نوظهور بر نقد شوندگی سهام با تأکید بر خصوصی سازی شرکت ها
-
تأثیر آمیخته بازاریابی پوشاک ایرانی بر تصویر ذهنی مشتری پوشاک ایرانی (هاکوپیان)
-
رهگیری شهاب سنگ ها
-
بررسی روشهای کاهش و حذف آلودگی نفتی (pahs) در آبهای دریا (خلیج فارس)
-
finite reasons for safety
-
mixed caputo fractional landau inequalities
-
numerical range of self-inverse matrices
مقالات جدیدترین ژورنال ها
-
مدیریت و بررسی افسردگی دانش آموزان دختر مقطع متوسطه دوم در دروان کرونا در شهرستان دزفول
-
مدیریت و بررسی خرد سیاسی در اندیشه ی فردوسی در ادب ایران
-
واکاوی و مدیریت توصیفی قلمدان(جاکلیدی)ضریح در موزه آستان قدس رضوی
-
بررسی تاثیر خلاقیت، دانش و انگیزه کارکنان بر پیشنهادات نوآورانه کارکنان ( مورد مطالعه: هتل های 3 و 4 ستاره استان کرمان)
-
بررسی تاثیر کیفیت سیستم های اطلاعاتی بر تصمیم گیری موفق در شرکتهای تولیدی استان اصفهان (مورد مطالعه: مدیران شرکتهای تولیدی استان اصفهان)
-
نقش سواد رسانه بر سواد سلامت زنان در استفاده از فضای مجازی مطالعه موردی: زنان شهرستان محمود آباد استان مازندران
-
آسایش در خانه مطالعه موردی: خانه تاریخی بهنام تبریز
-
مروری بر ادبیات نظری تجربی در خصوص تأثیر شرایط اقتصاد کلان بر ریسک حسابرسی
-
ارائه راهکارهای تامین منابع درآمدهای پایدار شهری مطالعه موردی: شهرداری مهاباد
-
مدل شناسایی و جذب فناوری های کلیدی در شرکت های کوچک تا متوسط (sme)
سوال خود را در مورد این مقاله مطرح نمایید :