Re: inference rule markup?

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