Abstract
A polarized version of Girard, Scedrov and Scott's Bounded Linear Logic is introduced and its normalization properties studied. Following Laurent [25], the logic naturally gives rise to a type system for the λμ-calculus, whose derivations reveal bounds on the time complexity of the underlying term. This is the first example of a type system for the λμ-calculus guaranteeing time complexity bounds for typable programs. © Springer-Verlag 2013.
Cite
CITATION STYLE
Dal Lago, U., & Pellitta, G. (2013). Complexity analysis in presence of control operators and higher-order functions. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 8312 LNCS, pp. 258–273). https://doi.org/10.1007/978-3-642-45221-5_19
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
