A metalanguage for cost-aware denotational semantics
Yue Niu, Robert Harper

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 of programming languages. Extending the recent work of Niu et al. [2022] on , a dependent type theory for both cost and behavioral verification, we define two metalanguages, and , for studying cost-aware metatheory. is an extension of with universes and inductive types, and is a an extension of 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 generalization of the classic Plotkin-type computational adequacy theorem. Moreover, by developing our proofs in a synthetic language of…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Logic, Reasoning, and Knowledge · Computability, Logic, AI Algorithms
