Cost-sensitive computational adequacy of higher-order recursion in synthetic domain theory
Rattachement africain : jp, gb, us. Niveau de preuve : code pays fourni par la source.
Le résumé fourni par la source
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. Comment: Final version for MFPS '24
Ce résumé expose les affirmations des auteurs. BNTIC ne l’interprète pas comme une validation indépendante des résultats.
Le contrôle bibliographique ouvert
DOI retrouvé dans Crossref DOI retrouvé ; titre concordant.
- Titre Crossref
- Cost-sensitive computational adequacy of higher-order recursion in synthetic domain theory
- Date Crossref
- 11/12/2024
- Éditeur
- Centre pour la Communication Scientifique Directe (CCSD)
- Type
- journal-article
Ce recoupement confirme des métadonnées liées au DOI. Il ne confirme ni la méthode ni les conclusions de l’étude, et il ne compte pas comme une seconde source scientifique indépendante.
Où se fait cette recherche
-
National Institute of Informatics pays non établi dans la noticeStructure de recherche
-
University of Cambridge pays non établi dans la noticeUniversité ou école supérieure
-
PRG S&Tech (South Korea) pays non établi dans la noticeEntreprise
-
Carnegie Mellon University pays non établi dans la noticeUniversité ou école supérieure
-
Department of Computer Science and Technology pays non établi dans la noticeInstitution
National Institute of Informatics, University of Cambridge et PRG S&Tech (South Korea), avec 2 autres affiliations.
Une affiliation ne permet pas de déduire la nationalité d’un auteur.