On Higher-Order Algebra
The purpose of this talk is to give an overview of recent work by myself
and students 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 and introduce the concept of second-order algebraic
theory. Theory morphisms lead to a mathematical definition of syntactic
translation that formalises notions such as encodings and transforms in
the context of languages with variable binding.
M.Fiore. Second-order and dependently-sorted abstract syntax. In
Proceedings of the 23rd Logic in Computer Science Conference (LICS'08),
pages 57-68, 2008.
M.Fiore and C.-K.Hur. Second-order equational logic. In Proceedings of
the 19th EACSL Annual Conference on Computer Science Logic (CSL 2010),
LNCS 6247, pp. 320-335, 2010.
M.Fiore and O.Mahmoud. Second-order algebraic theories. In Proceedings
of the 35th International Symposium on Mathematical Foundations of
Computer Science (MFCS 2010), LNCS 6281, pp. 368-380, 2010.