محبوبترین نویسندگان :
نویسندگان مقالات پربازدید :
مجله استدلال خودکار 2013
جزئیات رویداد
همایش ، رویداد ، ژورنال
اینستاگرام تی پی بین

  • locales: a module system for mathematical theories

    نویسندگان :
    کلمات کلیدی :
    جزئیات بیشتر مقاله
    • تاریخ ارائه: 1392/07/24
    • تاریخ انتشار در تی پی بین: 1392/07/24
    • تعداد بازدید: 778
    • تعداد پرسش و پاسخ ها: 0
    • شماره تماس دبیرخانه رویداد: -
     locales are a module system for managing theory hierarchies in a theorem prover through theory interpretation. they are available for the theorem prover isabelle. in this paper, their semantics is defined in terms of local theories and morphisms. locales aim at providing flexible means of extension and reuse. theory modules (which are called locales) may be extended by definitions and theorems. interpretation to isabelle’s global theories and proof contexts is possible via morphisms. even the locale hierarchy may be changed if declared relations between locales do not adequately reflect logical relations, which are implied by the locales’ specifications. by discussing their design and relating it to more commonly known structuring mechanisms of programming languages and provers, locales are made accessible to a wider audience beyond the users of isabelle. the discussed mechanisms include ml-style functors, type classes and mixins (the latter are found in modern object-oriented languages).

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

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