The precise control of inheritance and the inheritance of theory in the ADABTPL language

It is possible to include robust inheritance features while separating them from data structuring mechanisms to a higher degree than is accomplished in most languages. The ADABTPL language does this by supplying a small class of orthogonal inheritance producing and restricting mechanisms. ADABTPL also supports a paradigm of programming by tying the compiler to a powerful Boyer-Moore-style theorem prover that can be invoked by the programmer to verify properties of programs and validate program transformations. This is accomplished by the use of higher-order functions and metatheorems to produce a tailored theory about particular programs.<>