کد مقاله کد نشریه سال انتشار مقاله انگلیسی نسخه تمام متن
4662918 1345210 2013 29 صفحه PDF دانلود رایگان
عنوان انگلیسی مقاله ISI
Denotation of contextual modal type theory (CMTT): Syntax and meta-programming
ترجمه فارسی عنوان
دلالت نظریه نوع مودال متنی (CMTT): نحو و فرابرنامه ریزی
کلمات کلیدی
منطق موجهات 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
نویسندگان
, ,