W3C home > Mailing lists > Public > spec-prod@w3.org > January to March 2001

Re: inference rule markup?

From: Dan Connolly <connolly@w3.org>
Date: Wed, 14 Feb 2001 12:04:50 -0600
Message-ID: <3A8AC8C2.9715B640@w3.org>
To: Philip Wadler <wadler@research.bell-labs.com>
CC: Andrea Asperti <asperti@CS.UniBO.IT>, mff@research.att.com, spec-prod@w3.org, "Fuchs, Matthew" <matthew.fuchs@commerceone.com>, schena@CS.UniBO.IT, Claudio Sacerdoti_Coen <sacerdot@CS.UniBO.IT>, Luca Padovani <lpadovan@CS.UniBO.IT>, Ferruccio Guidi <fguidi@CS.UniBO.IT>
Philip Wadler wrote:
> 
> I would be interested in formalizing both MSL and the query algebra.
> 
>         MSL:
>         http://www.cs.bell-labs.com/who/wadler/topics/xml.html#msl
> 
>         Query algebra:
>         http://www.cs.bell-labs.com/who/wadler/topics/xml.html#xalgebra-icdt
>         http://www.w3.org/TR/query-algebra

Yes... exactly... me too; I see the latter is available as PDF;
I'd like to know how you produce it. I suspect you use latex
and some idioms/macros for grammars and inference rules
(and a few other notational idioms). If you'll point
me to some documentation of those tex/latex idioms
[I've been searching/surfing/googling without much luck]
and maybe let me look at the tex source of that algebra
paper, I'll try to design some XHTML/MathML dialect
that

	* can be machine-translated (using XSLT or something)
		to larch/coq/boomborg-pc for proof-checking

	* can be machine-translated to TeX for all the things
		that TeX is good for (printing, submitting to
		journals, etc.)

	* can be edited in direct-manipulation fashion with Amaya
		and/or Andrea's MathML editing tool and/or
		other XML editing tools.

oh... and of course, the semantic-web angle:

	* has its terms grounded in URI-space

-- 
Dan Connolly, W3C http://www.w3.org/People/Connolly/
Received on Wednesday, 14 February 2001 13:04:58 GMT

This archive was generated by hypermail 2.2.0+W3C-0.50 : Saturday, 10 March 2012 06:19:11 GMT