A metalanguage for cost-aware denotational semantics

TL;DR

This paper introduces two metalanguages, calf* and calfω, for developing cost-aware denotational semantics, enabling formal verification and analysis of program costs within a synthetic, phase-separated framework.

Contribution

It extends previous work on cost-aware type theory by defining new metalanguages and constructing denotational models for languages like simply-typed lambda calculus and Modernized Algol.

Findings

Constructed cost-aware denotational models satisfying a generalized adequacy theorem.

Developed a synthetic, phase-separated framework for cost analysis and verification.

Provided a positive answer to a conjecture on cost-aware semantics from prior work.

Abstract

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}^\omega$, for studying cost-aware metatheory. $\textbf{calf}^\star$ is an extension of $\textbf{calf}$ with universes and inductive types, and $\textbf{calf}^\omega$ 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.