The CakeML Verified Compiler and Toolchain
                            (Invited Talk)

                            Magnus O. Myreen

                Chalmers University of Technology, Sweden



  Abstract.
  The CakeML project has built an ecosystem of proofs and tools around
  an ML dialect called CakeML. The ecosystem includes a proven-correct
  compiler that can bootstrap itself within the logic of an interactive the-
  orem prover (HOL4).

  In this talk, I will give an overview of the entire ecosystem; I will show
  how HOL4 provides an architecture that scales to such large develop-
  ments; and I will explain where and how the CakeML project uses proof
  automation. The talk will conclude with a discuss of where I believe
  CakeML would gain most from improved proof automation.

  For more: https://cakeml.org/




                                      1