A Metalanguage for Cost-Aware Denotational Semantics

We present two metalanguages for developing synthetic cost-aware denotational semantics of programming languages. Extending the recent work of Niu et al. on calf, a dependent type theory for both cost and behavioral verification, we define two metalanguages, calf ★ and calf , for studying cost-aware metatheory. calf ★ is an extension of calf with universes and inductive types, and calf is a an extension of calf ★ 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 cost-aware generalization of the classic Plotkin-type computational adequacy theorem. Moreover, by developing our proofs in a synthetic language of phase-separated constructions of intension and extension, our results easily restrict to the corresponding extensional theorems. Consequently, our work provides a positive answer to the conjecture raised in Niu et al. [2022] and in light of 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.