From http://www.kindsoftware.com/products/opensource/OBJ3/
	 :	"OBJ" refers to the language family, while "OBJ2", "OBJ3", "CafeOBJ", etc. refer to particular members. The OBJ languages are broad spectrum algebraic programming and specification languages, based on order sorted equational logic, possibly enriched with other logics, such as rewriting logic or hidden equational logic. 

	 :	All the OBJ languages are rigorously based upon a logical system; more precisely, they are logical languages, in the sense that their programs are sets of sentences in some logical system, and their operational semantics is given by deduction in that logical system. All recent OBJ languages use order sorted algebra, which provides a rigorous basis for user definable sub-types, exception handling, multiple inheritance, overloading, multiple representations, coercions, and more. They also support user definable mixfix syntax, user definable execution strategies, rewriting modulo standard equational theories (AC, etc.), and selective memoization. 

	 :	All recent OBJ languages provide parameterized programming, with parameterized modules, module instantiation, views, module expressions, etc., to support very flexible program structuring and reuse. 

	 :	OBJ3 is based on order sorted equational logic, and has been successfully used for research and teaching in software design and specification, rapid prototyping, theorem proving, user interface design, and hardware verification, among other things. It was the first language to implement parameterized programming and its module system influenced the designs of the Ada, C++ and ML module systems. 
----
More information can be found at JosephGoguen's OBJ site (http://www-cse.ucsd.edu/users/goguen/sys/obj.html) or you can download OBJ3 from Joseph K's KindSoftware site (http://www.kindsoftware.com/products/opensource/OBJ3/).
----
CategoryProgrammingLanguage