Skip to Main content Skip to Navigation
New interface
Conference papers

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 metadata

Cited literature [27 references]  Display  Hide  Download
Contributor : Davide Sangiogi Connect in order to contact the contributor
Submitted on : Tuesday, November 26, 2013 - 10:46:40 AM
Last modification on : Wednesday, February 2, 2022 - 3:56:17 PM
Long-term archiving on: : Monday, March 3, 2014 - 4:11:59 PM


Files produced by the author(s)




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⟩



Record views


Files downloads