[TYPES/announce] Three papers.

[Marcelo Fiore]

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.