Automating Sized Type Inference for Complexity Analysis (Technical Report)

TL;DR

This paper presents an automated methodology for complexity analysis of higher-order functional programs using advanced type systems, monadic transformations, and constraint solving, capable of handling complex examples beyond existing methods.

Contribution

It introduces a fully automated approach combining size type inference, ticking monadic transformation, and constraint solving for higher-order program complexity analysis.

Findings

Successfully analyzes complex higher-order programs

Outperforms most existing methodologies in handling challenging examples

Prototype implementation demonstrates practical applicability

Abstract

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.