Yue Niu ; Jonathan Sterling ; Robert Harper - Cost-sensitive computational adequacy of higher-order recursion in synthetic domain theory

entics:14732 - Electronic Notes in Theoretical Informatics and Computer Science, December 11, 2024, Volume 4 - Proceedings of MFPS XL - https://doi.org/10.46298/entics.14732
Cost-sensitive computational adequacy of higher-order recursion in synthetic domain theoryArticle

Authors: Yue Niu ; Jonathan Sterling ; Robert Harper

    We study a cost-aware programming language for higher-order recursion dubbed $\textbf{PCF}_\mathsf{cost}$ in the setting of synthetic domain theory (SDT). Our main contribution relates the denotational cost semantics of $\textbf{PCF}_\mathsf{cost}$ 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 $\textbf{PCF}_\mathsf{cost}$ 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.


    Volume: Volume 4 - Proceedings of MFPS XL
    Published on: December 11, 2024
    Accepted on: November 13, 2024
    Submitted on: November 13, 2024
    Keywords: Computer Science - Programming Languages

    Consultation statistics

    This page has been seen 24 times.
    This article's PDF has been downloaded 11 times.