کد مقاله | کد نشریه | سال انتشار | مقاله انگلیسی | نسخه تمام متن |
---|---|---|---|---|
434190 | 689699 | 2014 | 21 صفحه PDF | دانلود رایگان |
عنوان انگلیسی مقاله ISI
Revisiting the categorical interpretation of dependent type theory
ترجمه فارسی عنوان
بازبینی تفسیر قطعی تئوری نوع وابسته
دانلود مقاله + سفارش ترجمه
دانلود مقاله ISI انگلیسی
رایگان برای ایرانیان
کلمات کلیدی
موضوعات مرتبط
مهندسی و علوم پایه
مهندسی کامپیوتر
نظریه محاسباتی و ریاضیات
چکیده انگلیسی
We show that Hofmann's and Curien's interpretations of Martin-Löf's type theory, which were both designed to cure a mismatch between syntax and semantics in Seely's original interpretation in locally cartesian closed categories, are related via a natural isomorphism. As an outcome, we obtain a new proof of the coherence theorem needed to show the soundness after all of Seely's interpretation.
ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Theoretical Computer Science - Volume 546, 21 August 2014, Pages 99–119
Journal: Theoretical Computer Science - Volume 546, 21 August 2014, Pages 99–119
نویسندگان
Pierre-Louis Curien, Richard Garner, Martin Hofmann,