کد مقاله | کد نشریه | سال انتشار | مقاله انگلیسی | نسخه تمام متن |
---|---|---|---|---|
8904286 | 1633416 | 2018 | 19 صفحه PDF | دانلود رایگان |
عنوان انگلیسی مقاله ISI
From realizability to induction via dependent intersection
ترجمه فارسی عنوان
از قابلیت اجرا به القاء از طریق تقاطع وابسته
دانلود مقاله + سفارش ترجمه
دانلود مقاله ISI انگلیسی
رایگان برای ایرانیان
موضوعات مرتبط
مهندسی و علوم پایه
ریاضیات
منطق ریاضی
چکیده انگلیسی
In this paper, it is shown that induction is derivable in a type-assignment formulation of the second-order dependent type theory λP2, extended with the implicit product type of Miquel, dependent intersection type of Kopylov, and a built-in equality type. The crucial idea is to use dependent intersections to internalize a result of Leivant's showing that Church-encoded data may be seen as realizing their own type correctness statements, under the Curry-Howard isomorphism.
ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Annals of Pure and Applied Logic - Volume 169, Issue 7, July 2018, Pages 637-655
Journal: Annals of Pure and Applied Logic - Volume 169, Issue 7, July 2018, Pages 637-655
نویسندگان
Aaron Stump,