Open AccessOn proving syntactic properties of CPS programs
Author(s) -
Olivier Danvy,
Belmina Dzafic,
Frank Pfenning
Publication year - 1999
Publication title -
brics report series
Language(s) - English
Resource type - Journals
eISSN - 1601-5355
pISSN - 0909-0878
DOI - 10.7146/brics.v6i23.20092
Subject(s) - transformation (genetics) , continuation , order (exchange) , arithmetic , mathematics , computer science , programming language , discrete mathematics , algebra over a field , pure mathematics , chemistry , biochemistry , finance , economics , gene
Higher-order program transformations raise new challenges for proving properties of their output, since they resist traditional, first-order proof techniques. In this work, we consider (1) the "one-pass" continuation-passing style (CPS) transformation, which is second-order, and (2) the occurrences of parameters of continuations in its output. To this end, we specify the one-pass CPS transformation relationally and we use the proof technique of logical relations.