Lambda the Ultimate

With the latest release of the Cat language inference of equirecursive function types (in Cat they are called "self" types) is now implemented. This means that in theory (this is not yet proven unfortunately) all valid Cat programs can be inferred. I was wondering what other languages with non-trivial type systems (e.g. they are able to discriminate higher order functions and different arities of functions) also have this property?

First, many thanks to LtU creator(s)/contributors, I have lurked profitably for a few years now. LtU readers are likely aware of Church's initial attempt to use the lambda calculus as a foundation for mathematics, and Curry's (and his students') subsequent attempts. But perhaps readers are unaware of this paper by Barendregt whose abstract contains the following:

These papers fulfil the program of Church and Curry to base logic on a consistent system of lambda-terms or combinators. Hitherto this program had failed because systems of ICL were either too weak (to provide a sound interpretation) or too strong (sometimes even inconsistent).

While the above announcement is unlikely to cause celebration in the streets, has it had any impact on the programming language or related math communities? I'm curious about the seeming lack of fanfare re the result (it was published in 98) and also about any existing or potential applications the result may have. I look forward to LtU experts to enlighten me (and likely many other interested LtU readers).