-
hybrid
جزئیات بیشتر مقاله- تاریخ ارائه: 1392/07/24
- تاریخ انتشار در تی پی بین: 1392/07/24
- تعداد بازدید: 707
- تعداد پرسش و پاسخ ها: 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.
مقالات جدیدترین رویدادها
-
استفاده از تحلیل اهمیت-عملکرد در ارائه الگوی مدیریت خلاقیت سازمانی و ارائه راهکار جهت بهبود
-
بررسی تاثیر ارزش وجوه نقد مازاد بر ساختار سرمایه شرکت های پذیرفته شده در بورس اوراق بهادار تهران
-
بررسی تأثیر سطح افشای ریسک بر قرارداد بدهی شرکت های پذیرفته شده در بورس اوراق بهادار تهران
-
بررسی تأثیر رتبه بندی اعتباری مبتنی بر مدل امتیاز بازار نوظهور بر نقد شوندگی سهام با تأکید بر خصوصی سازی شرکت ها
-
تأثیر آمیخته بازاریابی پوشاک ایرانی بر تصویر ذهنی مشتری پوشاک ایرانی (هاکوپیان)
-
نقدی بر جایگاه مذهب در سیر تحول تزیینات معماری ایران پس از اسلام
-
چگونگی شکل گیری جریان اصول گرایی در ایران پس از انقلاب اسلامی تا سال 1387
-
آسیب شناسی حاشیه نشینی و راهکارهای مدیریت شهری (نمونه موردی: محله شهرک سعدی شیراز)
-
بررسی عنصر هویتی رنگ در محور فرهنگی-تاریخی اصفهان
-
new algorithms for budgeted learning
مقالات جدیدترین ژورنال ها
-
مدیریت و بررسی افسردگی دانش آموزان دختر مقطع متوسطه دوم در دروان کرونا در شهرستان دزفول
-
مدیریت و بررسی خرد سیاسی در اندیشه ی فردوسی در ادب ایران
-
واکاوی و مدیریت توصیفی قلمدان(جاکلیدی)ضریح در موزه آستان قدس رضوی
-
بررسی تاثیر خلاقیت، دانش و انگیزه کارکنان بر پیشنهادات نوآورانه کارکنان ( مورد مطالعه: هتل های 3 و 4 ستاره استان کرمان)
-
بررسی تاثیر کیفیت سیستم های اطلاعاتی بر تصمیم گیری موفق در شرکتهای تولیدی استان اصفهان (مورد مطالعه: مدیران شرکتهای تولیدی استان اصفهان)
-
مهندسی ارزش مفاهیم، نظریه ها، تنگناها، چالشها
-
رتبه بندی عوامل موثر در برنامه ریزی موفق و ناموفق با استفاده از روش فرایند تحلیل سلسه مراتبی
-
تاثیر قوانین مالیات های مستقیم در جایگاه حاکمیت شرکتی
-
keeping the pulse of heritage awareness in ankara: two historic sites, two interventions
-
effects of steel fibers geometry on the mechanical properties of sifcon concrete
سوال خود را در مورد این مقاله مطرح نمایید :