From: Marcelo Fiore <Marcelo.Fiore@cl.cam.ac.uk>
To: categories@mta.ca
Subject: Three papers.
Date: Fri, 4 Jul 2008 14:19:41 +0100 (BST) [thread overview]
Message-ID: <E1KF6qe-00066C-4x@mailserv.mta.ca> (raw)
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.
reply other threads:[~2008-07-04 13:19 UTC|newest]
Thread overview: [no followups] expand[flat|nested] mbox.gz Atom feed
Reply instructions:
You may reply publicly to this message via plain-text email
using any one of the following methods:
* Save the following mbox file, import it into your mail client,
and reply-to-all from there: mbox
Avoid top-posting and favor interleaved quoting:
https://en.wikipedia.org/wiki/Posting_style#Interleaved_style
* Reply using the --to, --cc, and --in-reply-to
switches of git-send-email(1):
git send-email \
--in-reply-to=E1KF6qe-00066C-4x@mailserv.mta.ca \
--to=marcelo.fiore@cl.cam.ac.uk \
--cc=categories@mta.ca \
/path/to/YOUR_REPLY
https://kernel.org/pub/software/scm/git/docs/git-send-email.html
* If your mail client supports setting the In-Reply-To header
via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line
before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).