一句话：将依赖类型与线性类型系统结合，用定量类型论保证项的计算复杂度为多项式时间。
论文研究如何用类型系统同时表达依赖类型中的类型级任意计算与项级资源消耗，从而可靠且完备地刻画多项式时间计算。作者考察两种系统：一种禁止构造可迭代数据，另一种沿用 Hofmann 的 LFPL，通过“付费”机制控制数据构造。二者均借助定量类型论（Quantitative Type Theory）扩展到完整依赖类型。可靠性证明采用 Dal Lago 与 Hofmann 的 realizability 技术。长期目标是把类型论的外延推理与程序内在资源消耗的内涵推理结合，为资源分析工具和合成计算复杂度理论奠定基础。
We combine dependent types with linear type systems that soundly and completely capture polynomial time computation. We explore two systems for capturing polynomial time: one system that disallows construction of iterable data, and one, based on the LFPL system of Martin Hofmann, that controls construction via a payment method. Both of these are extended to full dependent types via Quantitative Type Theory, allowing for arbitrary computation in types alongside guaranteed polynomial time computation in terms. We prove the soundness of the systems using a realisability technique due to Dal Lago and Hofmann. Our long-term goal is to combine the extensional reasoning of type theory with intensional reasoning about the resources intrinsically consumed by programs. This paper is a step along this path, which we hope will lead both to practical systems for reasoning about programs’ resource usage, and to theoretical use as a form of synthetic computational complexity theory .