2017/06/28 by Martin Avanzini, Avanzini, Martin, Ugo Dal Lago +1
Computer Science · #Logic, programming, and type systems #Formal Methods in Verification #Parallel Computing and Optimization Techniques
paper · pdf · doi:10.48550/arxiv.1706.09169
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.