The second topic is a formulation of logical programming based on the first topic. Intuitively, a program is a theory over a formal logic, and its computation is deduction in that theory. The goal is to improve on Meseguer's formulation in his paper "General Logics" so as capture all the semantic facets of the BOBJ language as logical programming over various extensions of first order equational logic, including hidden equational logic.
The third topic is a categorical semantics of higher order module systems, again as implemented in BOBJ, especially for application to describing software architectures. This is based on a higher order extension of the categorical general systems theory of the author, by extending the diagram category construction to arbitrary orders.
Some version of these results will be reported in the paper Specifying, Programming and Verifying with Equational Logic, to appear in Festschrift volume for Dov Gabbay, along with a description of BOBJ's capability for mutual coinduction proofs.