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)
1
2

Abstract

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)
Loading...

Dates and versions

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

Identifiers

  • HAL Id : hal-01540760 , version 1

Cite

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

Share

Gmail Facebook Twitter LinkedIn More