2014/02/09 by Martin Hofmann, Hofmann, Martin, Georg Moser +1
Computer Science · #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Logic, programming, and type systems #Parallel Computing and Optimization Techniques #Programming Languages (cs.PL) #cs.LO #cs.PL
paper · pdf · doi:10.48550/arxiv.1402.1922
25 pages
openalex publication_date 2014/02/09 · arxiv created 2014/03/14 · arxiv updated 2014/03/17 · openalex created_date 2016/06/24 · openalex updated_date 2026/07/28
We introduce a novel resource analysis for typed term rewrite systems based on a potential-based type system. This type system gives rise to polynomial bounds on the innermost runtime complexity. We relate the thus obtained amortised resource analysis to polynomial interpretations and obtain the perhaps surprising result that whenever a rewrite system R can be well-typed, then there exists a polynomial interpretation that orients R. For this we adequately adapt the standard notion of polynomial interpretations to the typed setting.