Skip to content

Latest commit

 

History

History

proofs

Proofs files for compiling Pancake.

crep_arithProofScript.sml: Correctness proof for crep_arith pass

crep_to_loopProofScript.sml: Correctness proof for ---

loop_callProofScript.sml: loop_call proof

loop_liveProofScript.sml: Correctness proof for loop_live

loop_removeProofScript.sml: Correctness proof for loop_remove

loop_to_wordProofScript.sml: Correctness proof for loop_to_word

panItreeSemEquivScript.sml: Proof of correspondence between functional big-step and itree semantics for Pancake.

pan_simpProofScript.sml: Correctness proof for pan_simp

pan_to_crepProofScript.sml: Correctness proof for --

pan_to_targetProofScript.sml: composing semantics correctness from pan to target

pan_to_wordProofScript.sml: Correctness proof for combined pan_to_word compilation.

time: Proof files for compiling TimeLang.