Automating sized-type inference for complexity analysis

Martin Avanzini (1, 2) , Ugo Dal Lago (1, 3)

1 FOCUS - Foundations of Component-based Ubiquitous Systems
2 Leopold Franzens Universität Innsbruck - University of Innsbruck
3 DISI - Dipartimento di Scienze dell'Informazione [Bologna]

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.

Mots clés: Program analysis; Automated reasoning; Equational logic and rewriting; Functional languages

Domaines: Informatique [cs]; Logique en informatique [cs.LO]; Langage de programmation [cs.PL]

Martin Avanzini, Ugo Dal Lago. Automating sized-type inference for complexity analysis. Proceedings of the ACM on Programming Languages, 2017, 1 (ICFP), pp.1 - 29. ⟨10.1145/3110287⟩. ⟨hal-01639200⟩