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