一句话：提出基于广义逻辑关系的定量语义，构造笛卡尔闭的广义度量空间范畴，将欧氏度量扩展到高阶类型。
本文研究如何为简单类型 λ 演算这类高阶语言构建合适的广义度量语义。广义度量源于 Lawvere 将度量空间视为富集范畴的观点，在指称语义中可用于衡量两个程序行为相似但不等价的程度；然而将其应用于高阶语言一直不够理想。作者从通常逻辑关系的定量推广出发，提出一种构造广义度量空间笛卡尔闭范畴的新方法。在此框架下，他们证明若干族广义度量能够把欧氏度量从基本类型扩展到所有高阶类型，从而为高阶程序的相似性/距离提供统一的语义模型。评估以理论构造和证明为主，未报告实现或实验。
Generalized metrics, arising from Lawvere's view of metric spaces as enriched categories, have been widely applied in denotational semantics as a way to measure to which extent two programs behave in a similar, although non equivalent, way. However, the application of generalized metrics to higher-order languages like the simply typed lambda calculus has so far proved unsatisfactory. In this paper we investigate a new approach to the construction of cartesian closed categories of generalized metric spaces. Our starting point is a quantitative semantics based on a generalization of usual logical relations. Within this setting, we show that several families of generalized metrics provide ways to extend the Euclidean metric to all higher-order types.