کد مقاله | کد نشریه | سال انتشار | مقاله انگلیسی | نسخه تمام متن |
---|---|---|---|---|
4662918 | 1345210 | 2013 | 29 صفحه PDF | دانلود رایگان |
عنوان انگلیسی مقاله ISI
Denotation of contextual modal type theory (CMTT): Syntax and meta-programming
ترجمه فارسی عنوان
دلالت نظریه نوع مودال متنی (CMTT): نحو و فرابرنامه ریزی
دانلود مقاله + سفارش ترجمه
دانلود مقاله ISI انگلیسی
رایگان برای ایرانیان
کلمات کلیدی
منطق موجهات S4؛ مکاتبات کاری-هاوارد؛ نظریه نوع معین متنی؛ متا برنامه نویسی؛ منطق مرتبه بالاتر؛ نحو
موضوعات مرتبط
مهندسی و علوم پایه
ریاضیات
منطق ریاضی
چکیده انگلیسی
The modal logic S4 can be used via a Curry–Howard style correspondence to obtain a λ-calculus. Modal (boxed) types are intuitively interpreted as ‘closed syntax of the calculus’. This λ-calculus is called modal type theory—this is the basic case of a more general contextual modal type theory, or CMTT.CMTT has never been given a denotational semantics in which modal types are given denotation as closed syntax. We show how this can indeed be done, with a twist. We also use the denotation to prove some properties of the system.
ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Journal of Applied Logic - Volume 11, Issue 1, March 2013, Pages 1–29
Journal: Journal of Applied Logic - Volume 11, Issue 1, March 2013, Pages 1–29
نویسندگان
Murdoch J. Gabbay, Aleksandar Nanevski,