Using Intersection Types For Cost-Analysis Of Higher-Order Polymorphic Functional Programs

This paper presents a system of cost derivation for higher-order and polymorphic functional programs based on a notion of sized types and exploiting a type-and-effect system approach. The paper gives an operational semantics of cost for a simple strict functional language in terms of lambda-calculus beta-reduction steps and introduces type rules describing cost effects. The type system is based on intersection types. The use of discrete polymorphism (intersection types) instead of the usual parametric polymorphism approach improves the analysis and solves, in many cases, the "size aliasing problem" that has been identified as " limitation on previous type-and-effect approaches. Finally we provide " proof of the soundness of our effect system with respect to the cost semantics.