[CakeML-dev] Iterated bootstrap theorem?

Konrad Slind konrad.slind at gmail.com
Sat Feb 11 20:41:47 UTC 2017

I don't know much about this, but I vaguely recall Dave MacQueen
mentioning "T-diagrams" as a visual aid for reasoning about



On Fri, Feb 10, 2017 at 11:34 PM, Yong Kiam <tanyongkiam at gmail.com> wrote:

> Hi dev,
> This is more of a random question than anything. I was wondering if it is
> possible to get a theorem about k-fold bootstrap of the compiler, i.e.
> using the compiler to iterate compilation on itself once in the logic and
> k-1 times (outside the logic).
> Concretely, 1-fold bootstrap would be what we have right now, so the code
> being compiled in the logic looks like:
> ...
> val main str = print (compile conf str);
> A 2-fold bootstrap could look like:
> ...
> val cml_ast = ... //from an iterated translation of the compiler AST in
> HOL into a translated AST
> val main = print(compile conf (cml_ast));
> i.e. the output is a program, that when run, compiles the compiler AST.
> My sense is that such a k-fold bootstrap theorem could probably be done
> with what we have now (replace cml_ast with the appropriate n-1 th
> translation). The corresponding top-level correctness theorem would have
> some weird nested assumptions about each time the bootstrap is ran.
> One possible use of 2-fold bootstrap: one could evaluate in HOL using a
> fast (but less optimizing) version of the compiler, then turn on all the
> optimizations inside cml_ast. It probably doesn't matter for our bootstrap
> speed though.
> _______________________________________________
> Developers mailing list
> Developers at cakeml.org
> https://lists.cakeml.org/listinfo/developers
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.cakeml.org/pipermail/developers/attachments/20170211/b1c2654c/attachment.html>

More information about the Developers mailing list