# On Higher-Order Algebra

- 16:00 5th October 2010 ( week 0, Michaelmas Term 2010 )Lecture Theatre B

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.

References

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.

<http://www.cl.cam.ac.uk/~mpf23/papers/Types/AbsSyn.pdf>

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.

<http://www.cl.cam.ac.uk/~mpf23/papers/Types/soeqlog.pdf>

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.

<http://www.cl.cam.ac.uk/~mpf23/papers/Types/soat.pdf>