کد مقاله کد نشریه سال انتشار مقاله انگلیسی نسخه تمام متن
421624 684923 2015 19 صفحه PDF دانلود رایگان
عنوان انگلیسی مقاله ISI
A Model of Guarded Recursion With Clock Synchronisation
ترجمه فارسی عنوان
مدل بازگشت حفاظت شده با هماهنگ سازی ساعت
موضوعات مرتبط
مهندسی و علوم پایه مهندسی کامپیوتر نظریه محاسباتی و ریاضیات
چکیده انگلیسی

Guarded recursion is an approach to solving recursive type equations where the type variable appears guarded by a modality to be thought of as a delay for one time step. Atkey and McBride proposed a calculus in which guarded recursion can be used when programming with coinductive data, allowing productivity to be captured in types. The calculus uses clocks representing time streams and clock quantifiers which allow limited and controlled elimination of modalities. The calculus has since been extended to dependent types by Møgelberg. Both works give denotational semantics but no rewrite semantics.In previous versions of this calculus, different clocks represented separate time streams and clock synchronisation was prohibited. In this paper we show that allowing clock synchronisation is safe by constructing a new model of guarded recursion and clocks. This result will greatly simplify the type theory by removing freshness restrictions from typing rules, and is a necessary step towards defining rewrite semantics, and ultimately implementing the calculus.

ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Electronic Notes in Theoretical Computer Science - Volume 319, 21 December 2015, Pages 83-101