Correctness of static flow analysis in continuation semantics

AbstractWe show how restructuring a denotational definition leads to a more efficient compiling algorithm. Two semantics-preserving transformations (static replacement and factoring) are used to convert a continuation semantics into a formal description of a semantic analyzer and translator. The translation algorithm derived below performs type checking before code generation so that type-checking instructions may be omitted from the target code. The translation is proved correct with respect to the original definition of the source language. The proof consists of showing that both transformations preserve the semantics of the source language