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 "int").


	Makarius





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.