Merge pull request #1051 from CakeML/pancake_itree2

Pancake itree semantics
CakeML · Sep 9, 2024 · 3b5f1f0 · 3b5f1f0
2 parents 541fc6d + eca3504
commit 3b5f1f0
Show file tree

Hide file tree

Showing 5 changed files with 6,840 additions and 0 deletions.
diff --git a/pancake/proofs/README.md b/pancake/proofs/README.md
@@ -18,6 +18,10 @@ Correctness proof for loop_remove
 [loop_to_wordProofScript.sml](loop_to_wordProofScript.sml):
 Correctness proof for loop_to_word
 
+[panItreeSemEquivScript.sml](panItreeSemEquivScript.sml):
+Proof of correspondence between functional big-step
+and itree semantics for Pancake.
+
 [pan_simpProofScript.sml](pan_simpProofScript.sml):
 Correctness proof for pan_simp