Efficient first order functional program interpreter with time bound certifications

Jean-Yves Marion 1 Jean-Yves Moyen 1
1 CALLIGRAMME - Linear logic, proof networks and categorial grammars
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : We demonstrate that the class of functions computed by first order functional programs over lists which terminate by multiset path ordering and admit a polynomial quasi-interpretation, is exactly the class of function computable in polynomial time. The interest of this result lies on (i) the simplicity of the conditions on programs to certify their complexity, (ii) the fact that an important class of natural programs is captured, (iii) potential applications for program optimization.
Mots-clés : analyse complexité program transformation runtime analysis transformation programmes
Type de document :
Communication dans un congrès
M. Parigot & A. Voronkov. International Conference on Logic Programming & Automated Reasoning - LPAR'2000, Nov 2000, Reunion Island, France, Springer-Verlag, 1955, pp.25-42, 2000, Lecture Notes in Computer Science
Liste complète des métadonnées
https://hal.inria.fr/inria-00099178
Contributeur : Publications Loria <>
Soumis le : mardi 26 septembre 2006 - 08:51:33
Dernière modification le : jeudi 11 janvier 2018 - 06:19:48

Identifiants

  • HAL Id : inria-00099178, version 1

Collections

INRIA | LORIA | UNIV-LORRAINE

Citation

Jean-Yves Marion, Jean-Yves Moyen. Efficient first order functional program interpreter with time bound certifications. M. Parigot & A. Voronkov. International Conference on Logic Programming & Automated Reasoning - LPAR'2000, Nov 2000, Reunion Island, France, Springer-Verlag, 1955, pp.25-42, 2000, Lecture Notes in Computer Science. 〈inria-00099178〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

82

Contact


archive-ouverte@inria.fr