Skip to Main content Skip to Navigation
Journal articles

Automating sized-type inference for complexity analysis

Martin Avanzini 1, 2 Ugo Dal Lago 1, 3
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.
Complete list of metadata

Cited literature [2 references]  Display  Hide  Download
Contributor : Ugo Dal Lago Connect in order to contact the contributor
Submitted on : Monday, November 20, 2017 - 1:03:41 PM
Last modification on : Friday, October 30, 2020 - 12:04:03 PM
Long-term archiving on: : Wednesday, February 21, 2018 - 3:32:50 PM


Files produced by the author(s)




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



Record views


Files downloads