Do CPS translations also translate realizers? - Ecole Centrale de Marseille Accéder directement au contenu
Communication Dans Un Congrès Année : 2023

Do CPS translations also translate realizers?

Samuel Gardelle
  • Fonction : Auteur
  • PersonId : 1209085
Étienne Miquey

Résumé

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 rst 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.
Fichier principal
Vignette du fichier
main-long.pdf (557.51 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)

Dates et versions

hal-03910311 , version 1 (22-12-2022)
hal-03910311 , version 2 (31-03-2023)

Identifiants

  • HAL Id : hal-03910311 , version 1

Citer

Samuel Gardelle, Étienne Miquey. Do CPS translations also translate realizers?. JFLA 2023 - 34èmes Journées Francophones des Langages Applicatifs, Jan 2023, Praz-sur-Arly, France. pp.134-151. ⟨hal-03910311v1⟩

Collections

JFLA2023
197 Consultations
119 Téléchargements

Partager

Gmail Facebook X LinkedIn More