[isabelle-dev] CakeML compiler in the AFP

Makarius makarius at sketis.net
Fri Sep 21 14:36:16 CEST 2018

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.


More information about the isabelle-dev mailing list