### Abstract

This entry contains the formalization that accompanies my PhD thesis (see https://lars.hupel.info/research/codegen/). I develop a verified compilation toolchain from executable specifications in Isabelle/HOL to CakeML abstract syntax trees. This improves over the state-of-the-art in Isabelle by providing a trustworthy procedure for code generation.

### License

BSD License

### Topics

- Computer science/Programming languages/Compiling
- Logic/Rewriting

### Session CakeML_Codegen

- ML_Utils
- Compiler_Utils
- Code_Utils
- CakeML_Utils
- Test_Utils
- Doc_Terms
- Terms_Extras
- HOL_Datatype
- Constructors
- Consts
- Strong_Term
- Sterm
- Pterm
- Term_as_Value
- Value
- Doc_CupCake
- CupCake_Env
- CupCake_Semantics
- Doc_Rewriting
- General_Rewriting
- Rewriting_Term
- Rewriting_Nterm
- Rewriting_Pterm_Elim
- Rewriting_Pterm
- Rewriting_Sterm
- Big_Step_Sterm
- Big_Step_Value
- Big_Step_Value_ML
- Doc_Preproc
- Eval_Class
- Embed
- Eval_Instances
- Doc_Backend
- CakeML_Setup
- CakeML_Backend
- CakeML_Correctness
- CakeML_Byte
- Doc_Compiler
- Composition
- Compiler
- Test_Composition
- Test_Print
- Test_Embed_Data
- Test_Embed_Data2
- Test_Embed_Tree
- Test_Datatypes

### Depends on

- CakeML
- Constructor Functions
- Dictionary Construction
- An Algebra for Higher-Order Terms
- The Textbook Proof of Huffman’s Algorithm
- Pairing Heap
- Root-Balanced Tree
- Haskell’s Show Class in Isabelle/HOL

### Auto-related entries

- Light-weight Containers
- XML
- Imperative Insertion Sort
- Native Word

## Cite

×

CakeML_Codegen-AFP

    @article{CakeML_Codegen-AFP,
      author  = {Lars Hupel},
      title   = {A Verified Code Generator from Isabelle/HOL to CakeML},
      journal = {Archive of Formal Proofs},
      month   = {July},
      year    = {2019},
      note    = {\url{https://isa-afp.org/entries/CakeML_Codegen.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 18, 2020 : Isabelle2020
- Jul 11, 2019 : Isabelle2019