Re: [Haskell-cafe] Safe lists with GADT's

Hi

Coq does have termination checking, and Neil Mitchell is working on a case-and-termination checker for Haskell.

I was working on a case and termination checker. Now I'm just working on a case checker (which is pretty much done). The main reason I gave up on termination is that it was done very nicely in: J. Giesl, S. Swiderski, P. Schneider-Kamp, and R. Thiemann Automated Termination Analysis for Haskell: From Term Rewriting to Programming Languages In Proceedings of the 17th International Conference on Rewriting Techniques and Applications (RTA '06), Seattle, USA, Lecture Notes in Computer Science 4098, pages 297-312, 2006. Thanks Neil