Complexity Analysis in Presence of Control Operators and Higher-Order Functions (Long Version)
classification
💻 cs.LO
cs.PL
keywords
complexityboundslambda-mu-calculuslogicsystemtimetypeversion
pith:3FCPXAFN Add to your LaTeX paper
What is a Pith Number?\usepackage{pith}
\pithnumber{3FCPXAFN}
Prints a linked pith:3FCPXAFN badge after your title and writes the identifier into PDF metadata. Compiles on arXiv with no extra files. Learn more
read the original 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.
This paper has not been read by Pith yet.
discussion (0)
Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.