Re: [isabelle] ML in LCF architecture



On Thu, 20 Jan 2011, mark at proof-technologies.com wrote:

Funnily, when Mark encountered the Isabelle tty for the first time some months ago, his first impulse was to drop out of the managed Isar environment, in order to have raw access to the underlying ML :-)

Yes this is how I understand how things really work. Maybe I'm just a low-level command line junkie :-)

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.


	Makarius





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