Séminaire Cambium, Inria Paris, 2 rue Simone Iff
                          Salle Lions 1, bâtiment C
                          Vendredi 13 octobre, 09h00

                               Magnus O. Myreen
                      Chalmers University of Technology

                             The CakeML Project:
                Verified Compilation, Verified Bootstrapping,
                  Just-In-Time Compilation, and Applications

This talk will be about the CakeML project. The CakeML project centres
around an impure functional programming language, for which we have
developed a collection of proofs and tools inside the HOL4 theorem
prover. The development includes a proven-correct compiler that can
bootstrap itself.

This talk has two parts.

In the first part, I will explain the research questions the CakeML
project has tackled and outline the main research ideas that have
helped us address them. The research questions include:
 - how can we transfer properties proved of logic functions to
   properties of machine code compiled from those functions?
 - how can we use a verified compiler to compile itself?
 - how can we reason about space usage of CakeML programs?
 - how can we prove liveness properties for non-terminating code?

In the second part, I will describe how the CakeML project strives to
build meaningful connections with other projects and our experience
with this so far. We have:
 - built a proved-to-be-sound clone of the HOL light theorem prover
 - produced a verified compiler for a Haskell-like language
 - constructed several verified checkers, including checkers for UNSAT
   proofs, floating-point error bounds, OpenTheory article files,
   pseudo-Boolean proofs, and Integer Programming proofs

The CakeML project is a collaborative open source project and we
are always keen to explore new directions and collaborations.

The CakeML webpage: https://cakeml.org/

The CakeML project lives in the HOL4 theorem prover:
https://hol-theorem-prover.org/

            Vous pouvez vous abonner à nos annonces de séminaires:
                     http://cambium.inria.fr/seminar.html

             Nos séminaires sont accessibles en ligne en direct:
                     https://bbb.inria.fr/pot-xb8-cq4-y6w