Dependently Typed programming languages such as Agda and Idris2, and to some extent Coq and Lean, allow a "very strongly typed" kind of functional programming. Their expressive type systems allow programmers to write detailed specifications for their programs that constrain and guide the programming experience, and provide verified guarantees about program behaviour.

However, these specifications can only express extensional properties of programs -- properties relating the "what" of programs, but not the "how". For example, it is not possible to directly state that a particular function executes in polynomial time.

I will present an extension to dependent type theory, based on linear types, that allows expression of properties like "polynomial time" within the language. I'll explain how the system works, and how to prove its soundness. Finally, I'll explain some consequences of such a system, and the kinds of complexity theory we can build upon it.