Lambda the Ultimate

Proving the Correctness of Reactive Systems Using Sized Types, John Hughes, Lars Pareto, Amr Sabry. 1996.

We have designed and implemented a type-based analysis
for proving some basic properties of reactive systems. The
analysis manipulates rich type expressions that contain information
about the sizes of recursively defined data structures.
Sized types are useful for detecting deadlocks, nontermination,
and other errors in embedded programs. To
establish the soundness of the analysis we have developed
an appropriate semantic model of sized types.

Recursion and Dynamic Data-structures in Bounded Space: Towards Embedded ML Programming, John Hughes, Lars Pareto. 1999.

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 constructs 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.

Continuing the series on total functions and termination, a couple of papers co-authored by someone who can tell you why functional programming matters. The first paper introduces a type system that uses sized types to track termination, productivity and liveness properties for algebraic and coalgebraic data. The second papers extends the system to track memory regions and other space effects.

Previously mentioned on LtU quite a few times, but only on comments.