Re: [isabelle] ML in LCF architecture

On Thu, 20 Jan 2011, mark at wrote:

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?

Yes, the ML inside Isar is the full Poly/ML moderated by some of our infrastructure. It is a bit like an operating system that turns the raw CPU and memory into virtualized versions, such that user space programs cannot mess up the whole thing, and the whole system becomes much more useful and powerful than bare metal.


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