> 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.
Of course. I'm aware and we're emailing back and forth.
But this is to some extent orthogonal to Fabian's effort
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 progr
