Theorem Prover for complexity theoretic reductions
This is certainly possible, and the language of higher order functions makes this quite nice. If you're doing a Turing/Cook reduction, you can basically just write a function that takes an oracle as a parameter.

For example, to show that Graph Coloring is NP-hard, you could write something like this (pardon my terrible Coq-like pseudocode)

Theorem reduction: 
  (forall (k:Nat) (g:Graph), Decidable (Coloring g))
  -&gt; (forall (f:BoolFormula), Decidable (Model f))


What gets tricky is proving that your reductions are polynomial-time. There are ways to do this, such as with a time-tracking monad. This example verifies the time complexity of a sorting algorithm, and gives some hints as to how to model this. Basically, for whatever operation you're counting as $O(1)$, you require that it be performed in the monad, as well as calls to your oracle. Then you write a proof of some polynomial bound on the number of operations performed in the monad (which can keep track of them by encapsulating state).