Skip to Main content Skip to Navigation
Journal articles

Theory of Higher Order Interpretations and Application to Basic Feasible Functions

Emmanuel Hainry 1 Romain Péchoux 1
1 MOCQUA - Designing the Future of Computational Models
Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
Abstract : Interpretation methods and their restrictions to polynomials have been deeply used to control the termination and complexity of first-order term rewrite systems. This paper extends interpretation methods to a pure higher order functional language. We develop a theory of higher order functions that is well-suited for the complexity analysis of this programming language. The interpretation domain is a complete lattice and, consequently, we express program interpretation in terms of a least fixpoint. As an application, by bounding interpretations by higher order polynomials, we characterize Basic Feasible Functions at any order.
Complete list of metadata
Contributor : Romain Péchoux Connect in order to contact the contributor
Submitted on : Wednesday, January 6, 2021 - 11:36:55 AM
Last modification on : Tuesday, January 25, 2022 - 11:44:06 AM


Files produced by the author(s)




Emmanuel Hainry, Romain Péchoux. Theory of Higher Order Interpretations and Application to Basic Feasible Functions. Logical Methods in Computer Science, Logical Methods in Computer Science Association, 2020, 16 (4), pp.25. ⟨10.23638/LMCS-16(4:14)2020⟩. ⟨hal-02499206v2⟩



Les métriques sont temporairement indisponibles