Quasi-interpretation Synthesis by Decomposition : An application to higher-order programs

Guillaume Bonfante 1 Jean-Yves Marion 1 Romain Péchoux 1
1 CARTE - Theoretical adverse computations, and safety
Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
Abstract : Quasi-interpretations have shown their interest to deal with resource analysis of first order functional programs. There are at least two reasons to study the question of modularity of quasi-interpretations. Firstly, modularity allows to decrease the complexity of the quasi-inter\-pretation search algorithms. Secondly, modularity allows to increase the intentionality of the quasi-interpretation method, that is the number of captured programs. In particular, we take advantage of modularity conditions to extend smoothly quasi-interpretations to higher order programs. In this paper, we study the modularity of quasi-interpretations through the notions of constructor-sharing and hierarchical unions. We show that in the case of constructor-sharing and hierarchical unions, the existence of quasi-interpretations is no longer a modular property. However, we can still certify the complexity of programs.
Type de document :
Communication dans un congrès
ICTAC, Sep 2007, Macao, China. Springer, 2007, LNCS
Liste complète des métadonnées

https://hal.inria.fr/inria-00130920
Contributeur : Romain Péchoux <>
Soumis le : mercredi 14 février 2007 - 14:00:33
Dernière modification le : jeudi 11 janvier 2018 - 06:21:25
Document(s) archivé(s) le : mardi 6 avril 2010 - 23:55:47

Fichier

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

Identifiants

  • HAL Id : inria-00130920, version 1

Collections

Citation

Guillaume Bonfante, Jean-Yves Marion, Romain Péchoux. Quasi-interpretation Synthesis by Decomposition : An application to higher-order programs. ICTAC, Sep 2007, Macao, China. Springer, 2007, LNCS. 〈inria-00130920〉

Partager

Métriques

Consultations de la notice

326

Téléchargements de fichiers

105