کد مقاله کد نشریه سال انتشار مقاله انگلیسی نسخه تمام متن
423740 685285 2008 16 صفحه PDF دانلود رایگان
عنوان انگلیسی مقاله ISI
A Bidirectional Refinement Type System for LF
موضوعات مرتبط
مهندسی و علوم پایه مهندسی کامپیوتر نظریه محاسباتی و ریاضیات
پیش نمایش صفحه اول مقاله
A Bidirectional Refinement Type System for LF
چکیده انگلیسی

We present a system of refinement types for LF in the style of recent formulations where only canonical forms are well-typed. Both the usual LF rules and the rules for type refinements are bidirectional, leading to a straightforward proof of decidability of type-checking even in the presence of intersection types. Because we insist on canonical forms, structural rules for subtyping can now be derived rather than being assumed as primitive. We illustrate the expressive power of our system with several examples in the domain of logics and programming languages.

ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Electronic Notes in Theoretical Computer Science - Volume 196, 22 January 2008, Pages 113-128