Re: inference rule markup?

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/