• nested abstract syntax in coq

    جزئیات بیشتر مقاله
    • تاریخ ارائه: 1392/07/24
    • تاریخ انتشار در تی پی بین: 1392/07/24
    • تعداد بازدید: 649
    • تعداد پرسش و پاسخ ها: 0
    • شماره تماس دبیرخانه رویداد: -
     we illustrate nested abstract syntax as a high-level alternative representation of languages with binding constructs, based on nested datatypes. our running example is a partial solution in the coq proof assistant to the poplmark challenge. the resulting formalization is very compact and does not require any extra library or special logical apparatus. along the way, we propose an original, high-level perspective on environments.

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

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