Re: inference rule markup?

Hi Andrea,

How pleasing to encounter someone I know from the world of semantics
now in the world of XML!  The HELM work looks very interesting.  Please
take a look at MSL, and let me know what you think about how easy or
hard it would be to formalize in HELM/COQ.

  http://www.cs.bell-labs.com/who/wadler/topics/xml.html

Currently we are trying to maintain the MSL document in HTML, and that
is a big mess.  Appropriate MathML tools would be a big step up.  And
the chance to directly verify properties of the formalism from the
same data that is published would be a huge step up.  (Babbage designed
the analytic engine so that it would typeset log and trig tables
directly, to avoid the possibility of transcription error.)

Cheers,  -- P