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. *)