Re: [isabelle] OpenTheory import for Isabelle



> Being able to use the CakeML definitions in Isabelle via OpenTheory would
> be very useful to us at CMU as well, allowing us to do all our work in
> Isabelle instead of pulling in HOL4 as well with all the obvious
> implications on trusted computed base size.

Nice to hear that you're also interested in this! Keep in mind though
that there are currently some technical issues preventing CakeML to be
exported to OpenTheory (<https://github.com/CakeML/cakeml/issues/321>).

Cheers
Lars




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