Do CPS translations also translate realizers?
Abstract
In the realm of the proofs-as-programs correspondence, continuation-passing style (CPS) translations are known to be twofold: they bring both a program translation and a logical translation. In particular, when using the former to compile a language with a control operator, the latter ensures the soundness of the compilation with respect to types. This work is inspired by [OS08], in which Oliva and Streicher explained how Krivine realizability could be rephrased as the composition of a CPS and an intuitionistic realizability model. In this paper, we propose to push one step forward the analysis of the relation between realizability models and CPS translations to investigate the following question: assume that two realizability models are defined using the source and the destination of a CPS translation, is it the case that the CPS translates realizers of a given formula into realizers of the translated formulas? Evidenced frames Before introducing evidenced frames, we give a first example of a (very standard) realizability interpretation that will serve both as the destination of the CPS translation considered in the sequel and as an introducing example for evidenced frames.
Origin : Files produced by the author(s)