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 : Saturday, October 16, 2021 - 11:26:10 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⟩



Record views


Files downloads