The geometry of types

Ugo Dal Lago 1, 2 Barbara Petit 3
2 FOCUS - Foundations of Component-based Ubiquitous Systems
CRISAM - Inria Sophia Antipolis - Méditerranée , DISI - Dipartimento di Informatica - Scienza e Ingegneria [Bologna]
Abstract : We show that time complexity analysis of higher-order functional programs can be effectively reduced to an arguably simpler (although computationally equivalent) verification problem, namely checking first-order inequalities for validity. This is done by giving an efficient inference algorithm for linear dependent types which, given a PCF term, produces in output both a linear dependent type and a cost expression for the term, together with a set of proof obligations. Actually, the output type judgement is derivable iff all proof obligations are valid. This, coupled with the already known relative completeness of linear dependent types, ensures that no information is lost, i.e., that there are no false positives or negatives. Moreover, the procedure reflects the difficulty of the original problem: simple PCF terms give rise to sets of proof obligations which are easy to solve. The latter can then be put in a format suitable for automatic or semi-automatic verification by external solvers. Ongoing experimental evaluation has produced encouraging results, which are briefly presented in the paper.
Type de document :
Communication dans un congrès
The 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '13, Proceedings, 2013, Rome, Italy. ACM, pp.167-178, 2013
Liste complète des métadonnées

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

https://hal.inria.fr/hal-00909318
Contributeur : Davide Sangiogi <>
Soumis le : mardi 26 novembre 2013 - 10:46:38
Dernière modification le : vendredi 20 avril 2018 - 15:44:24
Document(s) archivé(s) le : lundi 3 mars 2014 - 16:11:52

Fichier

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

Identifiants

  • HAL Id : hal-00909318, version 1

Collections

Citation

Ugo Dal Lago, Barbara Petit. The geometry of types. The 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '13, Proceedings, 2013, Rome, Italy. ACM, pp.167-178, 2013. 〈hal-00909318〉

Partager

Métriques

Consultations de la notice

237

Téléchargements de fichiers

602