[X-logic-www] [X-Logic] Re: OpenMind [12]

[Roger B. J. <rb...@rb...>]

Subject- Re: OpenMind
Url- http://www.rbjones.com/

Two core foundational propositions in X-Logic are, firstly that to give a
semantics to the full range of languages which can be represented in XML
(and that''s pretty much everything) you need a semantic foundation which is
equivalent to (or richer and stronger than) a mathematical foundation
system.

The secondary proposition is just that of the available candidates a
polymorphic higher order set theory is a pragmatic choice.

I don''t have a detailed knowledge of the literature, and I know of no-one
else who advocates mathematical foundation systems as a basis for XML
semantics (though its a pretty obvious idea).

However, the best evidence that this approach is reasonable is the
literature on HOL (which is itself such a foundation system), and I would
guess that the procedings of the TPHOLS conference series would be a good
place to look.

The term semantic embedding is a general term used for techniques for
realising proof support for some language using a semantically correct
mapping into HOL (or some other suitable logical system). Quite a few
languages have been treated in this way, including programming languages,
hardware description languages, and specification languages (such as CSP and
Z).

You have to bear in mind here that I am talking about strict formalisation,
in machine supported languages, not just a mathematical semantics.
Though category theory is often used for mathematical semantics, I am not
aware of it having being used for strictly formal semantics, and if you are
aware of this having been done I would be interested to have a reference.

For more information on HOL and the TPHOL conferences see:
http://www.cl.cam.ac.uk/Research/HVG/HOL/

Another source of information relevant to the connection between HOL and
programming languages is Tobias Nipkow''s isabelle/HOL tutorial, which
virtually presents HOL as a functional programming language.
(http://www.cl.cam.ac.uk/Research/HVG/Isabelle/dist/Isabelle99-1/doc/tutoria
l.pdf)

The foundation I advocate is classical set theory formalised in HOL, which
would be better than plain HOL if you wanted to do category theory in it.