Re: [isabelle] ML in LCF architecture



on 20/1/11 1:53 PM, Makarius <makarius at sketis.net> wrote:

> Fine.  So the next step is to see how raw ML implements Isar, and Isar
> incorporates ML again, with some sandboxing already in place.  You should
> then get some ideas how to implement a secure system, by adding
> appropriate infrastructure instead of chopping everything off as in
> HOL-Light, and probably also HOL Zero right now.

I'm not sure what you mean by "chopping everything off" ...

And are you saying that Isar currently incorporates full-blown ML, so that
users can write their own extensions with all the power of ML?

Mark.





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