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

Re: inference rule markup?

From: Philip Wadler <wadler@research.bell-labs.com>
Date: Wed, 28 Feb 2001 10:45:50 -0500
Message-Id: <200102281545.KAA8422788@nslocum.cs.bell-labs.com>
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 GMT

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