کد مقاله کد نشریه سال انتشار مقاله انگلیسی نسخه تمام متن
9656894 686056 2005 23 صفحه PDF دانلود رایگان
عنوان انگلیسی مقاله ISI
Transitivity in coercive subtyping
موضوعات مرتبط
مهندسی و علوم پایه مهندسی کامپیوتر نظریه محاسباتی و ریاضیات
پیش نمایش صفحه اول مقاله
Transitivity in coercive subtyping
چکیده انگلیسی
Coercive subtyping is a general approach to abbreviation and subtyping in dependent type theories with inductive types. Coherence and admissibility of transitivity are important both for understanding of the framework and for its correct implementation. In this paper, we study the issue of transitivity in the context of subtyping for parameterised inductive types. In particular, we propose and study the notion of weak transitivity and show that, for a large class of parameterised inductive types, the natural subtyping rules are coherent and weak transitivity is admissible in an intensional type theory. A possible extension of type theory with certain extensional computation rules is also discussed for achieving admissibility of transitivity in general.
ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Information and Computation - Volume 197, Issues 1–2, 25 February–15 March 2005, Pages 122-144
نویسندگان
, ,