Static Correctness of Hierarchical Procedures

A system of hierarchical, imperative, fully recursive types allows program fragments written for small types to be reused for all larger types. To exploit this property to enable type-safe hierarchical procedures, it is necessary to impose a static requirement on procedure calls. We introduce an example language and prove the existence of a sound requirement which preserves static correctness while allowing hierarchical procedures. This requirement is further shown to be optimal , in the sense that it imposes as few restrictions as possible. This establishes the theoretical basis for a very powerful and general type hierarchy with static type checking, which enables 1st order polymorphism and (multiple) inheritance in a language with assignments.