کد مقاله کد نشریه سال انتشار مقاله انگلیسی نسخه تمام متن
422234 685050 2008 17 صفحه PDF دانلود رایگان
عنوان انگلیسی مقاله ISI
Meta-programming With Built-in Type Equality
موضوعات مرتبط
مهندسی و علوم پایه مهندسی کامپیوتر نظریه محاسباتی و ریاضیات
پیش نمایش صفحه اول مقاله
Meta-programming With Built-in Type Equality
چکیده انگلیسی

We report our experience with exploring a new point in the design space for formal reasoning systems: the development of the programming language Ωmega. Ωmega is intended as both a practical programming language and a logic. The main goal of Ωmega is to allow programmers to describe and reason about semantic properties of programs from within the programming language itself, mainly by using a powerful type system.We illustrate the main features of Ωmega by developing an interesting meta-programming example. First, we show how to encode a set of well-typed simply typed λ-calculus terms as an Ωmega data-type. Then, we show how to implement a substitution operation on these terms that is guaranteed by the Ωmega type system to preserve their well-typedness.

ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Electronic Notes in Theoretical Computer Science - Volume 199, 24 February 2008, Pages 49-65