  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.
