Complexity Analysis in Presence of Control Operators and Higher-Order Functions (Long Version)
Logic in Computer Science
2013-10-08 v1 Programming Languages
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.
Cite
@article{arxiv.1310.1763,
title = {Complexity Analysis in Presence of Control Operators and Higher-Order Functions (Long Version)},
author = {Ugo Dal Lago and Giulio Pellitta},
journal= {arXiv preprint arXiv:1310.1763},
year = {2013}
}