cl-banner

Amortised Resource Analysis and Typed Polynomial Interpretations

Martin Hofmann and Georg Moser

Proceedings of the Joint 25th International Conference on Rewriting Techniques and Applications and 12th International Conference on Typed Lambda Calculi and Applications (RTA-TLCA 2014), Lecture Notes in Computer Science 8560, pp. 272 – 286, 2014.

Abstract

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.

 

  PDF |    doi:10.1007/978-3-319-08918-8_19  |  © Springer International Publishing Switzerland

BibTeX 

@inproceedings{MHGM-RTATLCA14,
author = "Martin Hofmann and Georg Moser",
title = "Amortised Resource Analysis and Typed Polynomial Interpretations",
booktitle = "Proceedings of the Joint 25th International Conference on
Rewriting Techniques and Applications and 12th
International Conference on Typed Lambda Calculi and Applications",
editor = "Gilles Dowek",
series = "Lecture Notes in Computer Science (Advanced Research in
Computing and Software Science)",
volume = 8560,
pages = "272--286",
year = 2014,
doi = "10.1007/978-3-319-08918-8_19"
}
Nach oben scrollen