### Abstract

CakeML is a functional programming language with a proven-correct compiler and runtime system. This entry contains an unofficial version of the CakeML semantics that has been exported from the Lem specifications to Isabelle. Additionally, there are some hand-written theory files that adapt the exported code to Isabelle and port proofs from the HOL4 formalization, e.g. termination and equivalence proofs.

### License

BSD License

### Topics

- Computer science/Programming languages/Language definitions

### Session LEM

- Lem_bool
- Lem_basic_classes
- Lem_tuple
- Lem_function
- Lem_maybe
- Lem_num
- LemExtraDefs
- Lem
- Lem_list
- Lem_either
- Lem_set_helpers
- Lem_set
- Lem_map
- Lem_string
- Lem_word
- Lem_show
- Lem_sorting
- Lem_relation
- Lem_pervasives
- Lem_function_extra
- Lem_assert_extra
- Lem_maybe_extra
- Lem_map_extra
- Lem_num_extra
- Lem_set_extra
- Lem_list_extra
- Lem_string_extra
- Lem_show_extra
- Lem_machine_word
- Lem_pervasives_extra

### Session CakeML

- Doc_Generated
- Lib
- Namespace
- FpSem
- Ast
- AstAuxiliary
- Ffi
- SemanticPrimitives
- SmallStep
- BigStep
- BigSmallInvariants
- Evaluate
- LibAuxiliary
- NamespaceAuxiliary
- PrimTypes
- SemanticPrimitivesAuxiliary
- SimpleIO
- Tokens
- TypeSystem
- TypeSystemAuxiliary
- Doc_Proofs
- Semantic_Extras
- Evaluate_Termination
- Evaluate_Clock
- Evaluate_Single
- Big_Step_Determ
- Big_Step_Total
- Big_Step_Fun_Equiv
- Big_Step_Unclocked
- Big_Step_Clocked
- Big_Step_Unclocked_Single
- Matching
- CakeML_Code
- CakeML_Quickcheck
- CakeML_Compiler
- Compiler_Test
- Code_Test_Haskell

### Depends on

- Finite Machine Word Library
- Coinductive
- A Formal Model of IEEE Floating Point Arithmetic
- Haskell’s Show Class in Isabelle/HOL

### Used by

- A Verified Code Generator from Isabelle/HOL to CakeML

### Auto-related entries

- Formalization of Generic Authenticated Data Structures

## Cite

×

CakeML-AFP

    @article{CakeML-AFP,
      author  = {Lars Hupel and Yu Zhang},
      title   = {CakeML},
      journal = {Archive of Formal Proofs},
      month   = {March},
      year    = {2018},
      note    = {\url{https://isa-afp.org/entries/CakeML.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
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018