کد مقاله کد نشریه سال انتشار مقاله انگلیسی نسخه تمام متن
4662043 1633471 2013 32 صفحه PDF دانلود رایگان
عنوان انگلیسی مقاله ISI
Combinatorial realizability models of type theory
ترجمه فارسی عنوان
مدل های قابل تحقق ترکیبی از نظریه نوع
کلمات کلیدی
امکان اجرا؛ چسب؛ روابط منطقی؛ نظریه نوع هموتوپی؛ تئوری نوع Martin-Löf؛ معناشناسی Groupoid
موضوعات مرتبط
مهندسی و علوم پایه ریاضیات منطق ریاضی
چکیده انگلیسی

We introduce a new model construction for Martin-Löf intensional type theory, which is sound and complete for the 1-truncated version of the theory. The model formally combines, by gluing along the functor from the category of contexts to the category of groupoids, the syntactic model with a notion of realizability. As our main application, we use the model to analyse the syntactic groupoid associated to the type theory generated by a graph G, showing that it has the same homotopy type as the free groupoid generated by G.

ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Annals of Pure and Applied Logic - Volume 164, Issue 10, October 2013, Pages 957–988
نویسندگان
, ,