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.

翻译：我们将依赖类型与能够可靠且完备地捕获多项式时间计算的线性类型系统相结合。我们探索了两种捕获多项式时间的系统：一种系统禁止构建可迭代数据，另一种系统基于Martin Hofmann的LFPL系统，通过支付方法控制构建。这两种系统都通过定量类型理论扩展为完整的依赖类型，使得在类型中可以进行任意计算，同时确保项的多项式时间计算。我们使用Dal Lago和Hofmann的可实现性技术证明了这些系统的可靠性。我们的长期目标是将类型理论的外延推理与程序内在消耗资源的內涵推理相结合。本文是沿着这条路径迈出的第一步，我们期望它既能催生用于推理程序资源使用情况的实用系统，又能作为合成计算复杂性理论的一种形式发挥理论作用。