کد مقاله کد نشریه سال انتشار مقاله انگلیسی نسخه تمام متن
422038 685008 2008 16 صفحه PDF دانلود رایگان
عنوان انگلیسی مقاله ISI
Multimodal Separation Logic for Reasoning About Operational Semantics
موضوعات مرتبط
مهندسی و علوم پایه مهندسی کامپیوتر نظریه محاسباتی و ریاضیات
پیش نمایش صفحه اول مقاله
Multimodal Separation Logic for Reasoning About Operational Semantics
چکیده انگلیسی

We show how to reason, in the proof assistant Coq, about realistic programming languages using a combination of separation logic and heterogeneous multimodal logic. A heterogeneous multimodal logic is a logic with several modal operators that are not required to satisfy the same frame conditions. The result is a powerful and elegant system for reasoning about programming languages and their semantics. The techniques are quite general and can be adopted to a wide variety of settings.

ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Electronic Notes in Theoretical Computer Science - Volume 218, 22 October 2008, Pages 5-20