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.

翻译：我们将依赖类型与能正确并且完全捕获多项式时间计算的线性类型系统相结合。我们探索了两种捕获多项式时间的系统：一种系统禁止构造可迭代数据，另一种基于马丁·霍夫曼的LFPL系统，通过支付方式控制构造。这两种系统均通过定量类型理论扩展至完整的依赖类型，允许在类型中进行任意计算，同时保证项中多项式时间计算的可实现性。我们采用达尔·拉戈与霍夫曼的可实现性技术证明了这些系统的正确性。我们的长期目标是将类型理论的外延推理与程序固有资源消耗的内涵推理相结合。本文将作为这一路径上的一个步骤，有望引领我们走向实践性的程序资源使用推理系统，并作为合成计算复杂性理论的一种形式为理论研究提供支持。