成本感知指称语义的元语言
摘要：使用两种金属语言来开发编程语言的“综合成本感知指示语义”。在刘牛等人[2022]关于$ extbf{calf}$的最新工作的基础上，我们定义了两种金属语言，$ extbf{calf}^star$和$ extbf{calf}^omega$，用于研究成本感知的元理论。$ extbf{calf}^star$是$ extbf{calf}$的扩展，包括宇宙和归纳类型，$ extbf{calf}^omega$是$ extbf{calf}^star$的扩展，包括无界迭代。我们构建了简单类型λ演算和现代化Algol的指示模型，并展示它们满足经典的Plotkin型计算相适应性定理的“成本感知”推广。此外，通过在一种“相分离”的内涵和外延构建的综合语言中开发我们的证明，我们的结果很容易“限制”到相应的外延定理。我们的工作对刘牛等人[2022]中提出的猜想给出了肯定的答案，并为同时进行成本感知编程、验证和编程语言的成本感知元理论提供了一种金属语言。
作者：Yue Niu, Robert Harper
论文ID：2209.12669
分类：Programming Languages
分类简称：cs.PL
提交时间：2022-09-27