Second-Order Algebraic Theories

DOI10.1007/978-3-642-15155-2_33MaRDI QIDQ3586098zbMATH OpenOpenAlexFDO

Authors Ola Mahmoud, Marcelo P. Fiore

Publication date 3 September 2010

Published in Mathematical Foundations of Computer Science 2010 (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1308.5409

Mathematics Subject Classification ID

Equational classes, universal algebra in model theory (03C05) Theories (e.g., algebraic theories), structure, and semantics (18C10)

Abstract: Fiore and Hur recently introduced a conservative extension of universal algebra and equational logic from first to second order. Second-order universal algebra and second-order equational logic respectively provide a model theory and a formal deductive system for languages with variable binding and parameterised metavariables. This work completes the foundations of the subject from the viewpoint of categorical algebra. Specifically, the paper introduces the notion of second-order algebraic theory and develops its basic theory. Two categorical equivalences are established: at the syntactic level, that of second-order equational presentations and second-order algebraic theories; at the semantic level, that of second-order algebras and second-order functorial models. Our development includes a mathematical definition of syntactic translation between second-order equational presentations. This gives the first formalisation of notions such as encodings and transforms in the context of languages with variable binding.

Recommendations

• Second-Order Equational Logic (Extended Abstract)
• Second-order arithmetic and the consistency of first-order theories
• On the algebraization of Henkin‐type second‐order logic
• scientific article; zbMATH DE number 1536018
• Transfinite type theory and provability of second order formulas
• Second-Order Logic and Foundations of Mathematics
• Separations of first and second order theories in bounded arithmetic
• Second-order and Inductive Definability on Finite Structures
• Encoding true second‐order arithmetic in the real‐algebraic structure of models of intuitionistic elementary analysis
• On essentially algebraic theories and their generalizations

Cited in

(19)

• An algebraic generalization of Frege structures -- binding algebras
• Theory and practice of second-order rewriting: foundation, evolution, and SOL
• The universal exponentiable arrow
• A complete equational axiomatisation of partial differentiation
• Formalization of universal algebra in Agda
• Nominal Lawvere theories: a category theoretic account of equational theories with names
• Formalizing CCS and \(\pi\)-calculus in Guarded Cubical Agda
• Second order equivalence of cardinals: An algebraic approach
• Second-Order Equational Logic (Extended Abstract)
• scientific article; zbMATH DE number 7379288 (Why is no real title available?)
• Complete algebraic semantics for second-order rewriting systems based on abstract syntax with variable binding
• High-level signatures and initial semantics
• Modular specification of monads through higher-order presentations
• scientific article; zbMATH DE number 7566074 (Why is no real title available?)
• How to prove decidability of equational theories with second-order computation analyser SOL
• Second-order unification in the presence of linear shallow algebraic equations
• Structured handling of scoped effects
• Clones, closed categories, and combinatory logic
• Two-dimensional Kripke semantics i: presheaves

This page was built for publication: Second-Order Algebraic Theories

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3586098)