Complexity Analysis in Presence of Control Operators and Higher-Order Functions (Long Version)

2013/10/07 by Ugo Dal Lago, Lago, Ugo Dal, Giulio Pellitta +1
Computer Science · #F.3.1 #F.3.2 #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems #Programming Languages (cs.PL) #cs.LO #cs.PL

paper · pdf · doi:10.48550/arxiv.1310.1763

arxiv created 2013/10/07 · openalex publication_date 2013/10/07 · arxiv updated 2013/10/08 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28

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.

Related

• Paths-based criteria and application to linear logic subsystems characterizing polynomial time
• A syntactical analysis of non-size-increasing polynomial time computation
• Typed lambda-calculi and superclasses of regular functions
• A New Proof of P-time Completeness of Linear Lambda Calculus
• On paths-based criteria for polynomial time complexity in proof-nets