Re: [isabelle] A beginner's questionu
On Thu, 25 Nov 2010, Francisco Ferreira wrote:
The first part with the motivation and the objectives presents the
subject in an attractive, yet realistic way (with the "The Sad Facts of
Just one note on the "The sad fact of life" about SML semantics.
The reference implementation http://www.mpi-sws.org/~rossberg/hamlet/ by
Andreas Rossberg can be understood as an executable version of that.
Nonetheless there are problems with it, because the static phase merely
checks that the problem is type-correct, without producing the resulting
type-assignment. As a consequence, the dynamic phase needs to be
implemented like a LISP interpreter, with explicit tags everywhere.
This archive was generated by a fusion of
Pipermail (Mailman edition) and