Proving running time upper bounds for algorithms in dependent type theory
As usual, (a) the high-level conceptual approach is basically the same as it is on paper, but (b) mechanization makes new things reasonable to attempt.

The way you do things is to define a cost semantics for a programming language, where you assign a cost for each of the operations in the language. Next, you define a machine model, with its own cost semantics assigning costs to each of the primitive machine operations. Next, you prove that translating programs into the machine model is cost-preserving, so that the language-level costs correspond to the machine-level costs.  

Then, you can take any particular program written in the language and prove things about its running time, memory usage, or whatever other costs your cost semantics tracks. You prove these things with math, the same as on paper. :) 

However, once you have a computer checking all the details of all your proofs, new things become possible. For example, it is fairly common in paper proofs to only give the machine cost model, and handwave the language and its cost model (people say "pseudocode" when they don't want to specify the details of the language). But this is only plausible when the language and machine are very close to each other, and when you don't care about constant factors. If you need the compiler to make nontrivial optimizations, or if you need to reason about exact (and not just asymptotic) complexity, then you need to be more precise about the language.

A good example of this is the CerCo project, which did verified compilation from C to microcontroller assembly in a way that enabled source-level reasoning about things like worst-case execution times.