OBJ3 ist ein Programm-Spezifikations- und Beweissysystem, das auf einer geordneten Gleichheitslogik beruht. Es wurde erfolgreich benutzt für Forschung und Lehre in Software-Design und -Spezifikation, Rapid Prototyping, Theorem-Beweiser, Design von Benutzerschnittstellen und Hardware-Verifikation. Es war die erste Sprache, die parametrisiertes Programmieren implementierte, und sein Modulsystem beeinflußte den Entwurf der Modulsysteme von Ada, C++ und ML. (hjb)