Recursion and Dynamic Data-structures in Bounded Space: Towards Embedded ML Programming

We present a functional language with a type system such that well typed programs run within stated space-bounds. The language is a strict, first-order variant of ML with con structs for explicit storage management. The type system is a variant of Tofte and Talpinʹs region inference system to which the notion of sized types) of Hughes, Pareto and Sabry, has been added.