Programming with equalities, subsorts, overloading, and parametrization in OBJ

Abstractobj is a declarative language, with mathematical semantics given by order-sorted equational logic and an operational semantics based on order-sorted term rewriting. obj also has user-definable abstract data types with mixfix syntax and a flexible type system that supports overloading and subtypes. In addition, obj has a powerful generic module mechanism, including nonexecutable “theories” as well as executable “objects”, plus “module expressions” that construct whole subsystems. Design and implementation choices for the obj interpreter are described here in detail