- From: Andrea Asperti <asperti@CS.UniBO.IT>
- Date: Fri, 16 Mar 2001 10:05:18 +0100 (CET)
- To: Philip Wadler <wadler@research.bell-labs.com>
- cc: Claudio Sacerdoti Coen <sacerdot@students.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>
Dear Philip, inside the library http://phd.cs.unibo.it/helm/html/library/ in the Rocq contrib you may find a full development of lambda-calculus in coq. Please note that this is not supported by specific notational stylesheets, at present, so html rendering is not quite satisfactory, but it can give you an idea of the expressive power of coq. Concerning our possible contribution, it looks like a lot of work with no clear "income" from our side. Our tool is under development, and we have other priorities, at present. Of course we may offer consulence, if required. HOWEVER, things would be different in case we could start a specific W3C-WG on these topics (and I would be glad to be among the promoters of this initiative). Please think of it! Best wishes. -- andrea On Wed, 28 Feb 2001, Philip Wadler wrote: > 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 Friday, 16 March 2001 04:05:35 UTC