This talk consists of brief informal summaries of progress on three recent topics. The first is a new formulation of the notion of institution with proof, showing how it really is an institution (in the variant sense), by using power ordered categories (joint work with Till Mossakowski). It is also suggested to avoid creating new terminology and large tuples of structures added to institutions in the original sense, just by using twisted relations over forgetful functors into sets.

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, particularly its extension of the diagram category construction to arbitrary orders. Related research by Duran and Meseguer treated the first order case in a similar way.

A sketch of these results is 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.

The slides for the presentation by Till Mossakowski and Joseph Goguen on