[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]
Dear All, this is to announce the three papers below available from the top of <http://www.cl.cam.ac.uk/~mpf23/latest.html>. Best regards, Marcelo. 1. M. Fiore and C.-K. Hur. On the construction of free algebras for equational systems. Submitted, 2008. Abstract. The purpose of this paper is threefold: to present a general abstract, yet practical, notion of equational system; to investigate and develop the finitary and transfinite construction of free algebras for equational systems; and to illustrate the use of equational systems as needed in modern applications. 2. M. Fiore and C.-K. Hur. Term Equational Systems and Logics. To appear in 24th Mathematical Foundations of Programming Semantics Conf. (MFPS XXIV), 2008. Abstract. We introduce an abstract general notion of system of equations between terms, called Term Equational System, and develop a sound logical deduction system, called Term Equational Logic, for equational reasoning. Further, we give an analysis of algebraic free constructions that together with an internal completeness result may be used to synthesise complete equational logics. Indeed, as an application, we synthesise a sound and complete nominal equational logic, called Synthetic Nominal Equational Logic, based on the category of Nominal Sets. Keywords. Equational systems, algebraic theories, free algebras, equational logic, soundness, completeness, Nominal Sets, Schanuel topos. 3. M. Fiore. Second-order and dependently-sorted abstract syntax. In Logic in Computer Science Conf. (LICS'08), pages 57-68. IEEE, Computer Society Press, 2008. Abstract. The paper develops a mathematical theory in the spirit of categorical algebra that provides a model theory for second-order and dependently-sorted syntax. The theory embodies notions such as alpha-equivalence, variable binding, capture-avoiding simultaneous substitution, term metavariable, meta-substitution, mono and multi sorting, and sort dependency. As a matter of illustration, a model is used to extract a second-order syntactic theory, which is thus guaranteed to be correct by construction.