Marcelo Fiore (Cambridge)

Algebraic Foundations for Type Theories

Over the past several years, I have been working on algebraic foundations for type theories. The general idea driving this research is to develop mathematical meta-theories for the algebraic modelling of both the syntax and semantics of type theories, with the aim to use these model-theoretic frameworks to synthesise logical frameworks; see [1]. This line of investigation has been explored in detail in the context of simple type theories [2, 3]. In this talk, I would like to reexamine this work and consider extensions of it in two orthogonal directions to respectively incorporate dependent type theories and polymorphic type theories. The associated mathematical development has applications to the formalisation of type theories and to dependently-typed programming.

References [1] M. Fiore. Algebraic meta-theories and synthesis of equational logics. Research programme, <http://www.cl.cam.ac.uk/~mpf23/EqMetaLog.pdf>, 2009. [2] M. Fiore and C.-K. Hur. Second-order equational logic. In Proceedings of the 19th EACSL Annual Conference on Computer Science Logic (CSL 2010), volume 6247 of Lecture Notes in Computer Science, pages 320–335. Springer-Verlag, 2010. [3] M. Fiore and O. Mahmoud. Second-order algebraic theories. In Proceedings of the 35th International Symposium on Mathematical Foundations of Computer Science (MFCS 2010), volume 6281 of Lecture Notes in Computer Science, pages 368–380. Springer-Verlag, 2010.