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 metadatas

Cited literature [2 references]  Display  Hide  Download

https://hal.inria.fr/hal-01639200
Contributor : Ugo Dal Lago <>
Submitted on : Monday, November 20, 2017 - 1:03:41 PM
Last modification on : Tuesday, April 16, 2019 - 3:08:06 PM
Long-term archiving on : Wednesday, February 21, 2018 - 3:32:50 PM

File

paper.pdf
Files produced by the author(s)

Identifiers

Collections

Citation

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⟩

Share

Metrics

Record views

454

Files downloads

112