[isabelle-dev] CakeML compiler in the AFP

[Makarius]

On 20/09/18 11:02, Lars Hupel wrote:
> 
> I'm considering putting the entire CakeML compiler somewhere so that it
> is accessible in the AFP.

Just a side-remark: Fabian Immler has started with some experiments to
use HOL4 with CakeML inside Isabelle. You should keep in contact with
him about progress and possibilities.

We can of course discuss such things on the isabelle-dev mailing, when
it is relevant to ongoing Isabelle development. Or even on the HOL
mailing list, when HOL4 things are touched.


	Makarius