I have been looking around, unsuccessfully, for generalizations of universal algebra based on higher-order logic (rather than first order) and where the relations are not purely equational. Motivation: I need a "theory of syntax" for presentations of higher-order, non-equational theories. Furthermore, I want to be able to specify 'combinators' over these presentations, rigorously.

I am aware of Lawvere theories, but these are still equational (and neither particularly higher-order, though the multi-sorted generalization seems straightforward enough). There is a beginning of model theory done in a logical independent way, i.e. model theory over an institution; but that seems to concentrate on the model-theoretic aspects, rather than the universal algebra aspects. Perhaps what I am looking for are sketches?

[Edit:] From the various answer below, it seems I should be asking the question "how can I view type theory as a theory of syntax"? Somehow, that seems like an 'implementation' (as it requires a fair bit of 'encoding'); for example, to express the 'theory of categories' [i.e. (Obj, Mor, id, src, trg, $\circ$) and 5-6 axioms, I need a dependent record. Plus what is a sort (and sort constructor for Mor), what is an operation, and what is in Prop? Universal algebra cleanly separates these.

A good question was asked: what theorems do I want? Well, whatever operations I make on theories, well-formedness of the results will require discharging some obligations -- these obligations should all be finitely expressible (and automatically well-formed). Furthermore, the resulting syntactic objects and their morphisms should form a finitely co-complete category. Note that I expect that deciding if a given (presentation of a ) theory has a model to be undecidable.

Sheaves in Geometry and Logicby MacLane and Moerdijk). Otherwise, you might find what you need inIntroduction to Higher Order Categorical Logicby Lambek and Scott. $\endgroup$ – François G. Dorais♦ Mar 11 '10 at 4:52