Cost-sensitive computational adequacy of higher-order recursion in synthetic domain theory
arxiv(2024)
摘要
We study a cost-aware programming language for higher-order recursion dubbed
PCF_𝖼𝗈𝗌𝗍 in the setting of synthetic domain theory (SDT).
Our main contribution relates the denotational cost semantics of
PCF_𝖼𝗈𝗌𝗍 to its computational cost semantics, a new kind of
dynamic semantics for program execution that serves as a mathematically natural
alternative to operational semantics in SDT. In particular we prove an
internal, cost-sensitive version of Plotkin's computational adequacy theorem,
giving a precise correspondence between the denotational and computational
semantics for complete programs at base type. The constructions and proofs of
this paper take place in the internal dependent type theory of an SDT topos
extended by a phase distinction in the sense of Sterling and Harper. By
controlling the interpretation of cost structure via the phase distinction in
the denotational semantics, we show that PCF_𝖼𝗈𝗌𝗍 programs
also evince a noninterference property of cost and behavior. We verify the
axioms of the type theory by means of a model construction based on relative
sheaf models of SDT.
更多查看译文
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要