Cost-sensitive computational adequacy of higher-order recursion in synthetic domain theory

Yue Niu, Jonathan Sterling, Robert Harper

We study a cost-aware programming language for higher-order recursion dubbed ${\text{PCF}}_{\mathsf{cost}}$ in the setting of synthetic domain theory (SDT). Our main contribution rel…