Scholarlink

The \(\mathbb {K}\) Framework is a state-of-the-art tool for designing and analyzing programming languages, relying on a frontend tool, kompile, to translate high-level \(\mathbb {K}\) definitions into a low-level Kore representation based on Matching Logic ( \(\mathbb{M}\mathbb{L}\) ). Currently, this compilation process lacks a formal specification, making it a trusted but unverified component in the toolchain. This paper addresses this gap by proposing a formal mechanism for obtaining the denotational semantics for \(\mathbb {K}\) definitions directly as \(\mathbb{M}\mathbb{L}\) theories. A strong feature of the proposed approach is that it respects the abstraction and modularity principles of \(\mathbb {K}\) .

错误：搜索内容不能为空，请输入英文关键词
错误：关键词超出字数限制，请精简
高级检索

\(\mathbb {K}\) Definitions as Matching Logic Theories, Formally

  • 会议论文

  • 发表日期：

    2026年

查看全文
  • Xiaohong Chen,
  • Horaţiu Cheval,
  • Dorel Lucanu,
  • Grigore Roşu

摘要

The \(\mathbb {K}\) Framework is a state-of-the-art tool for designing and analyzing programming languages, relying on a frontend tool, kompile, to translate high-level \(\mathbb {K}\) definitions into a low-level Kore representation based on Matching Logic ( \(\mathbb{M}\mathbb{L}\) ). Currently, this compilation process lacks a formal specification, making it a trusted but unverified component in the toolchain. This paper addresses this gap by proposing a formal mechanism for obtaining the denotational semantics for \(\mathbb {K}\) definitions directly as \(\mathbb{M}\mathbb{L}\) theories. A strong feature of the proposed approach is that it respects the abstraction and modularity principles of \(\mathbb {K}\) .