Re: inference rule markup?

Hi Phil,

	I did not realize it was ... you :-)
I have been thrown in the discussion by Dan in a somewhat 
abrupt way, and I must confess I am a bit puzzled.
Also, the url you gave me contains too many pointers...
What do you wish to formalize exactly?
Thanks for the clarification.

					-- andrea

P.S. I send the mail in CC to my "equipe". Once we
have understood the problem, we should be able to give
you an answer in a few days.

On Wed, 14 Feb 2001, Philip Wadler wrote:

> 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
> 
> 
>