The purpose of this talk is to give an overview of recent work on a mathematical theory of higher-order algebraic structure. Specifically, I will introduce a conservative extension of universal algebra and equational logic from first to second order that provides a model theory and formal deductive system for languages with variable binding and parameterised metavariables. Mathematical theories encompassed by the framework include the (untyped and typed) lambda calculus, predicate logic, integration, etc. Subsequently, I will consider the subject from the viewpoint of categorical algebra, introducing second-order algebraic theories and functorial models, and establishing correspondences between theories and presentations and between models and algebras. The concept of theory morphism leads to a mathematical definition of syntactic translation that formalises notions such as encodings and transforms in the context of languages with variable binding.

The recently developed technique of Bohrification associates to a (unital) C*-algebra

• the Kripke model, a presheaf topos, of its classical contexts;
• in this Kripke model a commutative C*-algebra, called the Bohrification
• the spectrum of the Bohrification as a locale internal in Kripke model.

Recently D. Pataraia introduced the notion of hocha (higher-order cylindric Heyting algebra) in connection with his solution of the problem ”does every Heyting algebra occur as Sub(1) in a topos?”. In this talk we focus on the relationship between hochas and topises: we show that there is an equivalence between (finitary) hochas and toposes satisfying a natural ”minimality” condi- tion, and in particular that the category of finitary hochas is nothing other than the ind-completion of the dual of the free topos.