Automating sized-type inference for complexity analysis - Archive ouverte HAL Access content directly
Journal Articles Proceedings of the ACM on Programming Languages Year : 2017

Automating sized-type inference for complexity analysis

(1, 2) , (1, 3)
1
2
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.
Fichier principal
Vignette du fichier
paper.pdf (838.86 Ko) Télécharger le fichier
Origin : Files produced by the author(s)
Loading...

Dates and versions

hal-01639200 , version 1 (20-11-2017)

Identifiers

Cite

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⟩
233 View
83 Download

Altmetric

Share

Gmail Facebook Twitter LinkedIn More