Higher-Order Interpretations and Program Complexity

Authors Patrick Baillot, Ugo Dal Lago



PDF
Thumbnail PDF

File

LIPIcs.CSL.2012.62.pdf
  • Filesize: 0.54 MB
  • 15 pages

Document Identifiers

Author Details

Patrick Baillot
Ugo Dal Lago

Cite AsGet BibTex

Patrick Baillot and Ugo Dal Lago. Higher-Order Interpretations and Program Complexity. In Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 16, pp. 62-76, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)
https://doi.org/10.4230/LIPIcs.CSL.2012.62

Abstract

Polynomial interpretations and their generalizations like quasi-interpretations have been used in the setting of first-order functional languages to design criteria ensuring statically some complexity bounds on programs. This fits in the area of implicit computational complexity, which aims at giving machine-free characterizations of complexity classes. In this paper, we extend this approach to the higher-order setting. For that we consider the notion of simply-typed term rewriting systems, we define higher-order polynomial interpretations for them and give a criterion ensuring that a program can be executed in polynomial time. In order to obtain a criterion flexible enough to validate interesting programs using higher-order primitives, we introduce a notion of polynomial quasi-interpretations, coupled with a simple termination criterion based on linear types and path-like orders.
Keywords
  • implicit complexity
  • higher-order rewriting
  • quasi-interpretations

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail