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.
Type de document :
Article dans une revue
Proceedings of the ACM on Programming Languages, ACM, 2017, 1 (ICFP), pp.1 - 29. 〈10.1145/3110287〉
Liste complète des métadonnées

Littérature citée [37 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01639200
Contributeur : Ugo Dal Lago <>
Soumis le : lundi 20 novembre 2017 - 13:03:41
Dernière modification le : samedi 27 janvier 2018 - 01:31:51
Document(s) archivé(s) le : mercredi 21 février 2018 - 15:32:50

Fichier

paper.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

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〉

Partager

Métriques

Consultations de la notice

390

Téléchargements de fichiers

31