Note on models of polarised intuitionistic logic - Archive ouverte HAL Access content directly
Preprints, Working Papers, ... Year :

Note on models of polarised intuitionistic logic

(1, 2)


Following renewed interest in duploids arising from the exponential comonad of linear logic (the construction describing polarised intuitionistic translations into linear logic), I summarise here various remarks: • about a decomposition of Girard's "boring" translation as the expression of call-by-value in call-by-name, dual to how thunks are used to express call-by-name in call-by-value • about the coincidence between linear CPS translations and Girard's translations of intuitionistic logic into linear logic, • about a completeness property of historical models of linear logic in the above context • about a rational reconstruction of these translations with the Linear Call-by-Push-Value.
Fichier principal
Vignette du fichier
ll-cbpv.pdf (275.59 Ko) Télécharger le fichier
Origin : Files produced by the author(s)

Dates and versions

hal-01540760 , version 1 (16-06-2017)


  • HAL Id : hal-01540760 , version 1


Guillaume Munch-Maccagnoni. Note on models of polarised intuitionistic logic. 2017. ⟨hal-01540760⟩
277 View
112 Download


Gmail Facebook Twitter LinkedIn More