• formalizing adequacy: a case study for higher-order abstract syntax

    جزئیات بیشتر مقاله
    • تاریخ ارائه: 1392/07/24
    • تاریخ انتشار در تی پی بین: 1392/07/24
    • تعداد بازدید: 932
    • تعداد پرسش و پاسخ ها: 0
    • شماره تماس دبیرخانه رویداد: -
     adequacy is an important criterion for judging whether a formalization is suitable for reasoning about the actual object of study. the issue is particularly subtle in the expansive case of approaches to languages with name-binding. in prior work, adequacy has been formalized only with respect to specific representation techniques. in this article, we give a general formal definition based on model-theoretic isomorphisms or interpretations. we investigate and formalize an adequate interpretation of untyped lambda-calculus within a higher-order metalanguage in isabelle/hol using the nominal datatype package. formalization elucidates some subtle issues that have been neglected in informal arguments concerning adequacy.

سوال خود را در مورد این مقاله مطرح نمایید :

با انتخاب دکمه ثبت پرسش، موافقت خود را با قوانین انتشار محتوا در وبسایت تی پی بین اعلام می کنم
مقالات جدیدترین رویدادها
مقالات جدیدترین ژورنال ها