[Haskell-cafe] resources on static analysis

[Maarten Faddegon]

Dear list,

I am interested in learning more about static analysis of Haskell code. 
Specifically of the relation between arguments of recursive and 
non-recursive calls.

For example if we look at the ++ function from Prelude:

	(++) []     ys = ys
	(++) (x:xs) ys = x : xs ++ ys

amongst others, we could infer the relations:

	ys_i+1     = ys_i
	(x:xs)_i+1 = xs_i

Searching the web I found several tools (HLint, Haskabelle, 
Sourcegraph), but I am interested in the theory behind this. If you 
could recommend a paper or a book on this topic I would be grateful.

Thanks,
   Maarten Faddegon