Proving running time upper bounds for algorithms in dependent type theory Proof assistants are a valuable tool for verifying
the correctness of proofs of mathematical theorems.

When dealing with proofs of correctness of algorithms,
one is not only interested on showing that the algorithm
indeed works correctly, but also on showing some upper
bound on the execution of the algorithm.

Can proof assistants based on dependent type theory be 
used in a natural way to prove upper bounds on the 
running time of algorithms (besides of course of 
proving their correctness)? What is the standard approach
to do so?

If such assistants are not appropriate, is there some 
other kind of proof assistant that can do the job? 

Obs: When I say time, I mean the complexity theorist notion 
of time, in the sense of number of steps in an idealized RAM machine.
I don't care about formalization of actual hardware and 
physical time. Therefore, although Neel Krishnaswami is interesting, 
I'm not accepting it because it is far more complicated than what 
I'm looking for.
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.