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.
Document type :
Conference papers
Complete list of metadatas

Cited literature [27 references]  Display  Hide  Download

https://hal.inria.fr/hal-00909319
Contributor : Davide Sangiogi <>
Submitted on : Tuesday, November 26, 2013 - 10:46:40 AM
Last modification on : Saturday, January 27, 2018 - 1:30:54 AM
Long-term archiving on : Monday, March 3, 2014 - 4:11:59 PM

File

lpar2013.pdf
Files produced by the author(s)

Identifiers

Collections

Citation

Ugo Dal Lago, Giulio Pellitta. Complexity Analysis in Presence of Control Operators and Higher-Order Functions. LPAR-19 - Logic for Programming, Artificial Intelligence, and Reasoning - 2013, 2013, Stellenbosch, South Africa. pp.258-273, ⟨10.1007/978-3-642-45221-5_19⟩. ⟨hal-00909319⟩

Share

Metrics

Record views

225

Files downloads

161