Two extended abstracts on (1) Second-Order Equational Logic and (2) Second-Order Algebraic Theories are available as follows. We'd be grateful for any comments, Marcelo. -------- (1) M.Fiore and C.-K.Hur. Second-Order Equational Logic. <http://www.cl.cam.ac.uk/~mpf23/papers/Types/soeqlog.pdf> To appear in Proceedings of the 19th EACSL Annual Conference on Computer Science Logic (CSL 2010), 2010. Abstract. We extend universal algebra and its equational logic from first to second order as follows. 1. We consider second-order equational presentations as specified by identities between second-order terms, with both variables and parameterised metavariables over signatures of variable-binding operators. 2. We develop an algebraic model theory for second-order equational presentations, generalising the semantics of (first-order) algebraic theories and of (untyped and simply-typed) lambda calculi. 3. We introduce a deductive system, Second-Order Equational Logic, for reasoning about the equality of second-order terms. Our development is novel in that this equational logic is synthesised from the model theory. Hence it is necessarily sound. 4. Second-Order Equational Logic is shown to be a conservative extension of Birkhoff’s (First-Order) Equational Logic. 5. Two completeness results are established: the semantic completeness of equational derivability, and the derivability completeness of (bidirectional) Second-Order Term Rewriting. (2) M.Fiore and O.Mahmoud. Second-order algebraic theories. <http://www.cl.cam.ac.uk/~mpf23/papers/Types/soat.pdf> To appear in Proceedings of the 35th International Symposium on Mathematical Foundations of Computer Science (MFCS 2010), 2010. 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. [For admin and other information see: http://www.mta.ca/~cat-dist/ ]