Mercurial > cpdt > repo
diff src/StackMachine.v @ 394:cc8d0503619f
Citations for continuations and unification
| author | Adam Chlipala <adam@chlipala.net> |
|---|---|
| date | Sun, 22 Apr 2012 15:51:03 -0400 |
| parents | d1276004eec9 |
| children | 05efde66559d |
line wrap: on
line diff
--- a/src/StackMachine.v Sun Apr 22 15:38:11 2012 -0400 +++ b/src/StackMachine.v Sun Apr 22 15:51:03 2012 -0400 @@ -814,7 +814,7 @@ Lemma tcompile_correct' : forall t (e : texp t) ts (s : vstack ts), tprogDenote (tcompile e ts) s = (texpDenote e, s). -(** While lemma [compile_correct'] quantified over a program that is the %``%#"#continuation#"#%''% for the expression we are considering, here we avoid drawing in any extra syntactic elements. In addition to the source expression and its type, we also quantify over an initial stack type and a stack compatible with it. Running the compilation of the program starting from that stack, we should arrive at a stack that differs only in having the program's denotation pushed onto it. +(** While lemma [compile_correct'] quantified over a program that is the %``%#"#continuation#"#%''~\cite{continuations}% for the expression we are considering, here we avoid drawing in any extra syntactic elements. In addition to the source expression and its type, we also quantify over an initial stack type and a stack compatible with it. Running the compilation of the program starting from that stack, we should arrive at a stack that differs only in having the program's denotation pushed onto it. Let us try to prove this theorem in the same way that we settled on in the last section. *)