Do CPS translations also translate realizers?
Samuel Gardelle, Étienne Miquey · HAL (Le Centre pour la Communication Scientifique Directe) · 2023
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 dened 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?