Static Methods to Check Low-Level Code for a Graph Reduction Machine

This thesis is about checking code for a graph-reduction machine computing by template instantiation. An equation-based static checking method for low-level code is proposed in this thesis. The checking can be performed without requiring any extra code annotations. Most ill-behaved programs can be rejected and most well-behaved programs can be accepted. The template code has no explicit information about data types but the static checker works by inferring low-level recursive types. We show compatibility between high-level and low-level type systems. We evaluate empirically the eff�ectiveness of checking to prevent failures. We investigate the low-level implementation of the static checker and how it can be made efficient.