Complexity Analysis in Presence of Control Operators and Higher-Order Functions

Ugo Dal Lago 1, 2 Giulio Pellitta 1, 2
2 FOCUS - Foundations of Component-based Ubiquitous Systems
CRISAM - Inria Sophia Antipolis - Méditerranée , DISI - Dipartimento di Informatica - Scienza e Ingegneria [Bologna]
Abstract : A polarized version of Girard, Scedrov and Scott's Bounded Linear Logic is introduced and its normalization properties studied. Following Laurent, the logic naturally gives rise to a type system for the lambda-mu-calculus, whose derivations reveal bounds on the time complexity of the underlying term. This is the first example of a type system for the lambda-mu-calculus guaranteeing time complexity bounds for typable programs.
Type de document :
Communication dans un congrès
Ken McMillan and Aart Middeldorp and Andrei Voronkov. LPAR-19 - Logic for Programming, Artificial Intelligence, and Reasoning - 2013, 2013, Stellenbosch, South Africa. Springer, 8312, pp.258-273, 2013, Lecture Notes in Computer Science. 〈10.1007/978-3-642-45221-5_19〉
Liste complète des métadonnées

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

https://hal.inria.fr/hal-00909319
Contributeur : Davide Sangiogi <>
Soumis le : mardi 26 novembre 2013 - 10:46:40
Dernière modification le : jeudi 11 janvier 2018 - 16:22:51
Document(s) archivé(s) le : lundi 3 mars 2014 - 16:11:59

Fichier

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

Identifiants

Collections

Citation

Ugo Dal Lago, Giulio Pellitta. Complexity Analysis in Presence of Control Operators and Higher-Order Functions. Ken McMillan and Aart Middeldorp and Andrei Voronkov. LPAR-19 - Logic for Programming, Artificial Intelligence, and Reasoning - 2013, 2013, Stellenbosch, South Africa. Springer, 8312, pp.258-273, 2013, Lecture Notes in Computer Science. 〈10.1007/978-3-642-45221-5_19〉. 〈hal-00909319〉

Partager

Métriques

Consultations de la notice

173

Téléchargements de fichiers

59