Polynomial Time and Dependent Types

Robert Atkey

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 syste…