论文标题
一种用于成本感知语义语义的金属语言
A metalanguage for cost-aware denotational semantics
论文作者
论文摘要
我们提供了两个用于开发$ \ textit {综合成本感知语义语义} $编程语言的金属语言。扩展了Niu等人的最新工作。 [2022]在$ \ textbf {calf} $上，一种用于成本和行为验证的因类型理论，我们定义了两个金属语言，$ \ textbf {calf}^\ star $ star $和$ \ textbf {calf}^ω$，用于研究Cost-aware aware Metatheory。 $ \ textbf {calf}^\ star $是$ \ textbf {calf} $带有宇宙和归纳类型的扩展，$ \ textbf {calf}^ω$是$ \ textbf {calf}^\ star^star^star^sater n ving nocked Iteceration的延伸。 我们构建了简单类型的lambda演算的指示模型和 现代化的Algol，一种具有一阶商店的语言，并在循环中，并表明它们满足了经典Plotkin型计算充分定理的$ \ textit {Cost-Aware} $概括。 此外，通过以合成语言来开发我们的证据 $ \ textIt {phase-parterated} $ intension and Extension的构造，我们的结果很容易$ \ textit {限制} $ to相应的扩展定理。 我们的工作为Niu等人提出的猜想提供了积极的答案。 [2022]和$ \ textit {op。 CIT。} $在算法分析方面的工作，为进行成本感知的编程和验证以及对编程语言的成本感知的元看作用做出了贡献。
We present two metalanguages for developing $\textit{synthetic cost-aware denotational semantics}$ of programming languages. Extending the recent work of Niu et al. [2022] on $\textbf{calf}$, a dependent type theory for both cost and behavioral verification, we define two metalanguages, $\textbf{calf}^\star$ and $\textbf{calf}^ω$, for studying cost-aware metatheory. $\textbf{calf}^\star$ is an extension of $\textbf{calf}$ with universes and inductive types, and $\textbf{calf}^ω$ is a an extension of $\textbf{calf}^\star$ with unbounded iteration. We construct denotational models of the simply-typed lambda calculus and Modernized Algol, a language with first-order store and while loops, and show that they satisfy a $\textit{cost-aware}$ generalization of the classic Plotkin-type computational adequacy theorem. Moreover, by developing our proofs in a synthetic language of $\textit{phase-separated}$ constructions of intension and extension, our results easily $\textit{restrict}$ to the corresponding extensional theorems. Our work provides a positive answer to the conjecture raised in Niu et al. [2022] and in light of $\textit{op. cit.}$'s work on algorithm analysis, contributes a metalanguage for doing both cost-aware programming and verification and cost-aware metatheory of programming languages.
