Higher-order interpretations and program complexity

Patrick Baillot 1, 2 Ugo Dal Lago 3, 4
1 PLUME - Preuves et Langages
LIP - Laboratoire de l'Informatique du Parallélisme
4 FOCUS - Foundations of Component-based Ubiquitous Systems
CRISAM - Inria Sophia Antipolis - Méditerranée , DISI - Dipartimento di Informatica - Scienza e Ingegneria [Bologna]
Abstract : Polynomial interpretations and their generalizations like quasi-interpretations have been used in the setting of first-order functional languages to design criteria ensuring statically some complexity bounds on programs [10]. This fits in the area of implicit computational complexity, which aims at giving machine-free characterizations of complexity classes. In this paper, we extend this approach to the higher-order setting. For that we consider simply-typed term rewriting systems [35], we define higher-order polynomial interpretations for them, and we give a criterion ensuring that a program can be executed in polynomial time. In order to obtain a criterion flexible enough to validate interesting programs using higher-order primitives, we introduce a notion of polynomial quasi-interpretations, coupled with a simple termination criterion based on linear types and path-like orders.
Type de document :
Article dans une revue
Information and Computation, Elsevier, 2016, 〈10.1016/j.ic.2015.12.008〉
Liste complète des métadonnées

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

Contributeur : Ugo Dal Lago <>
Soumis le : lundi 27 juin 2016 - 14:58:06
Dernière modification le : mardi 16 janvier 2018 - 15:35:29


Fichiers produits par l'(les) auteur(s)




Patrick Baillot, Ugo Dal Lago. Higher-order interpretations and program complexity. Information and Computation, Elsevier, 2016, 〈10.1016/j.ic.2015.12.008〉. 〈hal-01337728〉



Consultations de la notice


Téléchargements de fichiers