Second-order universal algebra and second-order equational logic respectively provide a model theory and a formal deductive system for languages with variable binding and parameterised metavariables. This dissertation completes the algebraic foundations of second-order languages from the viewpoint of categorical algebra.

In particular, the dissertation introduces the notion of second-order algebraic theory. A main role in the definition is played by the second-order theory of equality M, representing the most elementary operators and equations present in every second-order language. We show that M can be described abstractly via the universal property of being the free cartesian category on an exponentiable object. Thereby, in the tradition of categorical algebra, a second-order algebraic theory consists of a cartesian category M and a strict cartesian identity-on-objects functor M: M →M that preserves the universal exponentiable object of M.

At the syntactic level, we establish the correctness of our definition by showing a categorical equivalence between second-order equational presentations and second-order algebraic theories. This equivalence, referred to as the Second-Order Syntactic Categorical Type Theory Correspondence, involves distilling a notion of syntactic translation between second-order equational presentations that corresponds to the canonical notion of morphism between second-order algebraic theories. Syntactic translations provide a mathematical formalisation of notions such as encodings and transforms for second-order languages.

On top of the aforementioned syntactic correspondence, we furthermore establish the Second-Order Semantic Categorical Type Theory Correspondence. This involves generalising Lawvere’s notion of functorial model of algebraic theories to the second-order setting. By this semantic correspondence, second-order functorial semantics is shown to correspond to the model theory of second-order universal algebra.

We finally show that the core of the theory surrounding Lawvere theories generalises to the second order as well. Instances of this development are the existence of algebraic functors and monad morphisms in the second-order universe. Moreover, we define a notion of translation homomorphism that allows us to establish a 2-categorical type theory correspondence.