  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.
