Marcelo Fiore (University of Cambridge, UK), Second-Order Algebra and Generalised Polynomial Functors
Schedule
- Feb. 27, 2012, 15:00 - 16:00
Abstract
The theme of this work is algebraic structure in settings richer than that of universal algebra. In this talk, I will consider an example and foundations. Starting with the example, I will introduce Second-Order Algebra: the algebra of languages with variable binding. This I will study from the viewpoints of universal algebra (equational presentations and algebraic models), equational logic (second-order deduction and rewriting), and categorical algebra (algebraic theories and functorial semantics). In this context, as well as in more general algebraic settings for languages with polymorphism and dependency, generalised polynomial functors between presheaf categories arise as foundational structures. I will present their basic theory, including differentiation.
References
- 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.
- M.Fiore. Algebraic Foundations for Type Theories. Talk given at the 18th Workshop Types for Proofs and Programs (Types 2011), Bergen (Norway), 2011.
- M.Fiore. Generalised polynomial functors: Theory and applications. Preprint, 2012.
The theme of this work is algebraic structure in settings richer than that of universal algebra. In this talk, I will consider an example and foundations. Starting with the example, I will introduce Second-Order Algebra: the algebra of languages with variable binding. This I will study from the viewpoints of universal algebra (equational presentations and algebraic models), equational logic (second-order deduction and rewriting), and categorical algebra (algebraic theories and functorial semantics). In this context, as well as in more general algebraic settings for languages with polymorphism and dependency, generalised polynomial functors between presheaf categories arise as foundational structures. I will present their basic theory, including differentiation.
References
- 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.
- M.Fiore. Algebraic Foundations for Type Theories. Talk given at the 18th Workshop Types for Proofs and Programs (Types 2011), Bergen (Norway), 2011.
- M.Fiore. Generalised polynomial functors: Theory and applications. Preprint, 2012.