What is the current state of the art in solving the halting problem? Yes, I know it's uncomputable in the general case. What I want to know is what special cases have been solved, and if there is work ongoing on finding or developing more of them.

To be a little more explicit about the sort of thing I'm looking for, total functional language compilers have to approximate the halting problem, proving that your source code terminates or saying it can't thus prove it. Idris, as far as I can tell, just uses a "one argument must be structurally smaller on each recursive call" primitive-recursion checker*; Isabelle is more sophisticated, with 

datatype rosetree = Rose "'a rosetree list"

primrec rosemap :: "('a =&gt; 'b) =&gt; 'a rosetree =&gt; 'b rosetree" where
  "rosemap f (Rose as) = Rose (map (rosemap f) as)"


compiling fine despite the intermediate map on the recursive calls. Isabelle's fun mechanism seems even more powerful in terms of proving termination (although I can't think of a short, simple example for that off the top of my head).

Basically: how do these work? Are there papers or textbooks about the algorithms involved somewhere? Is finding heuristics for the halting problem a current research subject?

*If I'm wrong about this, please do let me know about that, too.
The question as asked is indeed very broad. I give a brief answer here: What are some comparative studies on program termination verification tools?, but that really barely scratches the surface.

I do have several remarks:


In general, once must distinguish between whole program analyses, which are powerful, but do not scale very well for realistic development, and modular analyses which are weaker, but have hope of being integrated in a development environment. Isabelle and Idris both take this approach. As a side note, I'm not sure if this Fuhs et al paper corresponds to the "out of the box" termination check for Isabelle, but it might be enlightening in terms of what the state of the art is.
Termination of higher-order typed programs is difficult, because it involves subtle interactions between the type system features, the inductive types involved, and the "guard condition" required for function definitions. The more complicated the termination check, the less trustworthy the system, since consistency depends on it! These slides by Barras go into some of the nasty details for the Coq system.
Termination for higher-order systems with side effects (references) is particularly nasty. In particular, types are not enough anymore, even in the absence of recursion, see e.g. Landin's knot.