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
Topics
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