- From: Philip Wadler <wadler@research.bell-labs.com>
- Date: Wed, 28 Feb 2001 10:45:50 -0500
- To: Claudio Sacerdoti Coen <sacerdot@students.cs.unibo.it>
- cc: Philip Wadler <wadler@research.bell-labs.com>, Andrea Asperti <asperti@CS.UniBO.IT>, mff@research.att.com, spec-prod@w3.org, "Fuchs, Matthew" <matthew.fuchs@commerceone.com>, schena@CS.UniBO.IT, Luca Padovani <lpadovan@CS.UniBO.IT>, Ferruccio Guidi <fguidi@CS.UniBO.IT>
Wow!! This is great! Thank you for taking the trouble to produce this example. Examples are an extraordinarily effective means of communication. From your example I can clearly see that Coq+HELM might indeed make it possible to use formal tools to produce parts of the MSL and XML Algebra specifications, which would be an enormous step forward. I'd like to ask you to push the example further, in a few directions. Can you show how HELM can be used to produce XML/HTML versions of the inference rules and the proofs from your example? Can you show how Coq handles variable binding and substitution? The obvious way to do this would be to extend your example to lambda calculus. Better yet would be simply typed lambda calculus, since this would correspond closely to many of the issues faced in formalizing MSL and the XML Query Algebra. Finally, an example of a proof based on the formlasim (such as your immpl_ok theorem) would be helpful. And, last but not least, if we decide to use Coq and HELM, what help or support will be available from your group? Many thanks again, -- P
Received on Wednesday, 28 February 2001 10:47:51 UTC