-
hybrid
جزئیات بیشتر مقاله- تاریخ ارائه: 1392/07/24
- تاریخ انتشار در تی پی بین: 1392/07/24
- تعداد بازدید: 705
- تعداد پرسش و پاسخ ها: 0
- شماره تماس دبیرخانه رویداد: -
combining higher-order abstract syntax and (co)-induction in a logical framework is well known to be problematic. we describe the theory and the practice of a tool called hybrid, within isabelle/hol and coq, which aims to address many of these difficulties. it allows object logics to be represented using higher-order abstract syntax, and reasoned about using tactical theorem proving and principles of (co)induction. moreover, it is definitional, which guarantees consistency within a classical type theory. the idea is to have a de bruijn representation of λ-terms providing a definitional layer that allows the user to represent object languages using higher-order abstract syntax, while offering tools for reasoning about them at the higher level. in this paper we describe how to use hybrid in a multi-level reasoning fashion, similar in spirit to other systems such as twelf and abella. by explicitly referencing provability in a middle layer called a specification logic, we solve the problem of reasoning by (co)induction in the presence of non-stratifiable hypothetical judgments, which allow very elegant and succinct specifications of object logic inference rules. we first demonstrate the method on a simple example, formally proving type soundness (subject reduction) for a fragment of a pure functional language, using a minimal intuitionistic logic as the specification logic. we then prove an analogous result for a continuation-machine presentation of the operational semantics of the same language, encoded this time in an ordered linear logic that serves as the specification layer. this example demonstrates the ease with which we can incorporate new specification logics, and also illustrates a significantly more complex object logic whose encoding is elegantly expressed using features of the new specification logic.
مقالات جدیدترین رویدادها
-
استفاده از تحلیل اهمیت-عملکرد در ارائه الگوی مدیریت خلاقیت سازمانی و ارائه راهکار جهت بهبود
-
بررسی تاثیر ارزش وجوه نقد مازاد بر ساختار سرمایه شرکت های پذیرفته شده در بورس اوراق بهادار تهران
-
بررسی تأثیر سطح افشای ریسک بر قرارداد بدهی شرکت های پذیرفته شده در بورس اوراق بهادار تهران
-
بررسی تأثیر رتبه بندی اعتباری مبتنی بر مدل امتیاز بازار نوظهور بر نقد شوندگی سهام با تأکید بر خصوصی سازی شرکت ها
-
تأثیر آمیخته بازاریابی پوشاک ایرانی بر تصویر ذهنی مشتری پوشاک ایرانی (هاکوپیان)
-
بررسی تاثیر نسبت ابعادی بر ضریب شکل پذیری قابهای خمشی فولادی
-
مروری بر بازاریابی داخلی و پیامدهای آن در سازمان ها
-
بررسی خرابی های رویه بتنی اپرون قدیم فرودگاه زاهدان (مطالعه موردی)
-
اکتشاف زونهای کارستی آبدار با استفاده از روش ژئوالکتریک مطالعه موردی منطقه سمیرم واقع در استان اصفهان
-
l-methionine modified dowex-50 ion-exchanger of reduced size for the separation and removal of cu(ii) and ni(ii) from aqueous solution
مقالات جدیدترین ژورنال ها
-
مدیریت و بررسی افسردگی دانش آموزان دختر مقطع متوسطه دوم در دروان کرونا در شهرستان دزفول
-
مدیریت و بررسی خرد سیاسی در اندیشه ی فردوسی در ادب ایران
-
واکاوی و مدیریت توصیفی قلمدان(جاکلیدی)ضریح در موزه آستان قدس رضوی
-
بررسی تاثیر خلاقیت، دانش و انگیزه کارکنان بر پیشنهادات نوآورانه کارکنان ( مورد مطالعه: هتل های 3 و 4 ستاره استان کرمان)
-
بررسی تاثیر کیفیت سیستم های اطلاعاتی بر تصمیم گیری موفق در شرکتهای تولیدی استان اصفهان (مورد مطالعه: مدیران شرکتهای تولیدی استان اصفهان)
-
ارزیابی کیفی اطلاعات اینترنتی در حوزه سلامت
-
موانع و کاستی های کنوانسیون ملل متحد در مورد حقوق دریاها در رابطه با مجادله با دزدی دریایی
-
بررسی ارتباطات اثربخش و سکوت سازمانی مطالعه موردی: سازمان آب و فاضلاب شهری خراسان جنوبی
-
مقایسه رفتار لرزه ای سازه فولادی بهسازی شده با سه نوع میراگر ویسکوز، تسلیمی و اصطکاکی در سازه های کوتاه مرتبه، میان مرتبه و بلند مرتبه
-
درآمدی بر مبانی مسئولیت سازمانی از نگاه اسلام
سوال خود را در مورد این مقاله مطرح نمایید :