Static Correctness of Hierarchical Procedures

A system of hierarchical, fully recursive types in a truly imperative language 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 general type hierarchy with static type checking, which enables 1st order polymorphism combined with multiple inheritance and specialization in a language with assignments. We extend the results to include opaque types. An opaque version of a type is di erent from the original but has the same values and the same order relations to other types. The opaque types allow a more exible poly...

• Type: Conference
• Year: 1990
• Where: ICALP
• Authors: Michael I. Schwartzbach
• Keywords: Hierarchical Procedures, ICALP 1990, Opaque Types, Programming Languages, Type-safe Hierarchical Procedures