کد مقاله کد نشریه سال انتشار مقاله انگلیسی نسخه تمام متن
423798 685291 2012 14 صفحه PDF دانلود رایگان
عنوان انگلیسی مقاله ISI
Towards a Common Categorical Semantics for Linear-Time Temporal Logic and Functional Reactive Programming
موضوعات مرتبط
مهندسی و علوم پایه مهندسی کامپیوتر نظریه محاسباتی و ریاضیات
پیش نمایش صفحه اول مقاله
Towards a Common Categorical Semantics for Linear-Time Temporal Logic and Functional Reactive Programming
چکیده انگلیسی

Linear-time temporal logic (LTL) and functional reactive programming (FRP) are related via a Curry–Howard correspondence. Based on this observation, we develop a common categorical semantics for a subset of LTL and its corresponding flavor of FRP. We devise a class of categorical models, called fan categories, that explicitly reflect the notion of time-dependent trueness of temporal propositions and a corresponding notion of time-dependent type inhabitance in FRP. Afterwards, we define the more abstract concept of temporal category by extending categorical models of intuitionistic S4. We show that fan categories are a special form of temporal categories.

ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Electronic Notes in Theoretical Computer Science - Volume 286, 24 September 2012, Pages 229-242