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?
This archive was generated by a fusion of
Pipermail (Mailman edition) and