- From: Philip Wadler <wadler@research.bell-labs.com>
- Date: Fri, 23 Feb 2001 17:52:21 -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>
Claudio, Thank you for your detailed discussion. There are several properties it would be desirable to have for a formal representation of typing rules. (0) To be able to typeset the rules from their representation. You discuss how this is possible. (1) To be able to create a type inference tree, and check that it corresponds to the rules. (2) To be able to prove formal properties of the type system, such as that each term has a most general type. (3) To prove that a given type inference algorithm is correct. (4) To be able to automatically derive a correct type inference algorithm. We also want to be able to write a dynamic semantics, for which similar questions arise. (0') To be able to typeset the rules from their representation. You discuss how this is possible. (1') To be able to create an exectution tree, and check that it corresponds to the rules. (2') To be able to prove formal properties of the dynamic semantics, such as that evaluation is deterministic. (3') To be able to implement an evaluator for the language, and show that it corresponds to the dynamic semantics. (4') To be able to automatically derive a correct evaluator. Which of these do you think should be possible with HELM? Cheers, -- P
Received on Friday, 23 February 2001 17:54:10 UTC