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

Ugo Dal Lago (1, 2) , Giulio Pellitta (1, 2)

1 DISI - Dipartimento di Scienze dell'Informazione [Bologna]
2 FOCUS - Foundations of Component-based Ubiquitous Systems

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.

Domaines: Informatique

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⟩