- From: Philip Wadler <wadler@research.bell-labs.com>
- Date: Wed, 14 Feb 2001 09:15:51 -0500
- To: Andrea Asperti <asperti@CS.UniBO.IT>
- cc: mff@research.att.com, spec-prod@w3.org, "Fuchs, Matthew" <matthew.fuchs@commerceone.com>, schena@CS.UniBO.IT
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 09:17:38 UTC