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