Re: [isabelle] ML in LCF architecture



On Thu, 20 Jan 2011, mark at proof-technologies.com 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.


	Makarius





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