2014/10/23 by Erika De Benedetti, De Benedetti, Erika, Simona Ronchi Della Rocca +1
Computer Science · #03D15 #Computational Complexity (cs.CC) #F.4 #F.4.1 #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems #acm:03D15 #cs.CC #cs.LO #msc:03D15
paper · pdf · doi:10.48550/arxiv.1410.6298
31 pages
arxiv created 2014/10/23 · openalex publication_date 2014/10/23 · arxiv updated 2014/10/24 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
One of the aims of Implicit Computational Complexity is the design of programming languages with bounded computational complexity; indeed, guaranteeing and certifying a limited resources usage is of central importance for various aspects of computer science. One of the more promising approaches to this aim is based on the use of lambda-calculus as paradigmatic programming language and the design of type assignment systems for lambda-terms, where types guarantee both the functional correctness and the complexity bound. Here we propose a system of stratified types, inspired by intersection types, where intersection is a non-associative operator. The system, called STR, is correct and complete for polynomial time computations; moreover, all the strongly normalizing terms are typed in it, thus increasing the typing power with respect to the previous proposals. Moreover, STR enjoys a stronger expressivity with respect to the previous system STA, since it allows to type a restricted version of iteration.