Definitions and theorems are named according to "On The Occurrence of Continuation Parameters in CPS Programs" (September 17, 1997) READ.ME ---------- This file corr.elf ---------- Var-validity of mixed stacks. Lemma: for all XXi Var-valid data-stacks Xi -> Xi is a XXi Var-valid mixed stack cpsBNF.elf ---------- BNF of continuation-passing style terms (extended) def1+5+fig4.elf ---------- Definition of Cont-validity for CPS terms def13.elf ---------- Definition of control-stack substitution def16.elf ---------- Definition of data-stack substitution def3+6+fig5.elf ---------- Definition of Var-validity of CPS terms dsBNF.elf ---------- BNF of direct-style terms examples.quy ---------- some test examples fig1.elf ---------- The left-to-right, call-by-value CPS transformation fig10.elf ---------- CPS abstract machine with a data stack fig11.elf ---------- Definition of Var-validity of data stacks fig12.elf ---------- CPS abstract machine with two stack fig13.elf ---------- Definition of Cont-validity of data stacks fig7.elf ---------- Bare, stackless CPS abstract machine fig8.elf ---------- CPS abstract machine with a control stack fig9.elf ---------- Definition of Cont-validity of control stacks lemma14.elf ---------- Lemma : Control-stack substitution lemma17.elf ---------- Lemma : Data-stack substitution Lemma : Double mixed-stack substitution lemma7.elf ---------- Lemma : Preservation of cont-validity under substitution lemma9.elf ---------- Lemma : Preservation of Var-validity under substitution load.sml ---------- sml file for loading elf files test.quy ---------- Elf queries used in Chapter 6 th10.elf ---------- Theorem : Var-validity under beta-reduction th15.elf ---------- Theorem : The control-stack and the bare machine are equivalent th18.elf ---------- Theorem : The data-stack and the bare machine are equivalent th2.elf ---------- Theorem : A result of cps transformation is cont-valid th4.elf ---------- Theorem : A result of cps transformation is var-valid th8.elf ---------- Theorem : Preservation of Cont-validity under beta-reduction