  This paper introduces a new methodology for the complexity analysis of
higher-order functional programs, which is based on three ingredients: a
powerful type system for size analysis and a sound type inference procedure for
it, a ticking monadic transformation, and constraint solving. Noticeably, the
presented methodology can be fully automated, and is able to analyse a series
of examples which cannot be handled by most competitor methodologies. This is
possible due to the choice of adopting an abstract index language and index
polymorphism at higher ranks. A prototype implementation is available.

Logic in Computer Science;Computational Complexity