From: Philip Wadler <wadler@research.bell-labs.com>

Date: Fri, 23 Feb 2001 17:52:21 -0500

Message-Id: <200102232252.RAA5170622@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>

Date: Fri, 23 Feb 2001 17:52:21 -0500

Message-Id: <200102232252.RAA5170622@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>

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, -- PReceived on Friday, 23 February 2001 17:54:10 UTC

*
This archive was generated by hypermail 2.3.1
: Tuesday, 6 January 2015 20:42:16 UTC
*