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

  • formal metatheory of programming languages in the matita interactive theorem prover

    نویسندگان :
    کلمات کلیدی :
    جزئیات بیشتر مقاله
    • تاریخ ارائه: 1392/07/24
    • تاریخ انتشار در تی پی بین: 1392/07/24
    • تعداد بازدید: 798
    • تعداد پرسش و پاسخ ها: 0
    • شماره تماس دبیرخانه رویداد: -
     this paper is a report about the use of matita, an interactive theorem prover under development at the university of bologna, for the solution of the poplmark challenge, part 1a. we provide three different formalizations, including two direct solutions using pure de bruijn and locally nameless encodings of bound variables, and a formalization using named variables, obtained by means of a sound translation to the locally nameless encoding. according to this experience, we also discuss some of the proof principles used in our solutions, which have led to the development of a generalized inversion tactic for matita.a

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

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