کد مقاله کد نشریه سال انتشار مقاله انگلیسی نسخه تمام متن
422039 685008 2008 12 صفحه PDF دانلود رایگان
عنوان انگلیسی مقاله ISI
The Interpretation of Intuitionistic Type Theory in Locally Cartesian Closed Categories – an Intuitionistic Perspective
موضوعات مرتبط
مهندسی و علوم پایه مهندسی کامپیوتر نظریه محاسباتی و ریاضیات
پیش نمایش صفحه اول مقاله
The Interpretation of Intuitionistic Type Theory in Locally Cartesian Closed Categories – an Intuitionistic Perspective
چکیده انگلیسی

We give an intuitionistic view of Seely's interpretation of Martin-Löf's intuitionistic type theory in locally cartesian closed categories. The idea is to use Martin-Löf type theory itself as metalanguage, and E-categories, the appropriate notion of categories when working in this metalanguage. As an E-categorical substitute for the formal system of Martin-Löf type theory we use E-categories with families (E-cwfs). These come in two flavours: groupoid-style E-cwfs and proof-irrelevant E-cwfs. We then analyze Seely's interpretation as consisting of three parts. The first part is purely categorical: the interpretation of groupoid-style E-cwfs in E-locally cartesian closed categories. (The key part of this interpretation has been type-checked in the Coq system.) The second is a coherence problem which relates groupoid-style E-cwfs with proof-irrelevant ones. The third is a purely syntactic problem: that proof-irrelevant E-cwfs are equivalent to traditional lambda calculus based formulations of Martin-Löf type theory.

ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Electronic Notes in Theoretical Computer Science - Volume 218, 22 October 2008, Pages 21-32