A metalanguage for cost-aware denotational semantics
share
We present two metalanguages for developing synthetic cost-aware denotational semantics of programming languages. Extending the recent work of Niu et al. [2022] 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. 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.
READ FULL TEXT