Very Precise Static Analysis of Functional Languages

We look at fundamental properties of a technique for very precisely analyzing functional languages, that we call higher-rank polyvariance. In particular, we want to find out when the problem of achieving this level of precision is decidable, and when it is not. We also investigate how to best implement such analyses and how they can be proven to be correct.