Re: [isabelle] lexical matters
On Tue, 18 Jan 2011, mark at proof-technologies.com wrote:
We could harden Isabelle/ML against this, since the ML environment is
under our control.
How could this be done?
Dvid Matthews kindly provides ways in Poly/ML to manage the whole
compilation process in user space, including printing and binding of the
results. One would merely have to protect agains shadowing of certain
structure names, say.
When you've showed me an early version of HOL0 in Cambridge ITP 2009, I
have already pointed out that OCaml is not the best platform for that (due
to its mutable strings and silently overflowing machine words called
This archive was generated by a fusion of
Pipermail (Mailman edition) and