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

Re: inference rule markup?

From: Andrea Asperti <asperti@CS.UniBO.IT>
Date: Wed, 14 Feb 2001 16:07:47 +0100 (CET)
To: Philip Wadler <wadler@research.bell-labs.com>
cc: 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>
Message-ID: <Pine.LNX.4.21.0102141600580.17477-100000@marcello.cs.unibo.it>


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
> 
> 
> 
Received on Wednesday, 14 February 2001 10:08:02 GMT

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