■ Reference. Cost-Aware Type Theory [niu-harper-2020]