Higher-order size checking without subtyping

Abstract

This work focuses on checking size annotations of higher-order polymorphic functional programs supporting nested lists. These annotations are in a lambda-calculus that formalize non-linear and non-monothonic polynomial relations between the sizes of arguments and those of the corresponding results of functions. The presented sizing rules straightforwardly define verification condition generation. Since exact size dependencies are considered (i.e. without subtyping), checking of these conditions amounts to checking conditional equations between polynomials. © 2013 Springer-Verlag.