Note on models of polarised intuitionistic logic

Guillaume Munch-Maccagnoni 1, 2
1 GALLINETTE - Gallinette : vers une nouvelle génération d'assistant à la preuve
Inria Rennes – Bretagne Atlantique , LS2N - Laboratoire des Sciences du Numérique de Nantes
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.
Complete list of metadatas

Cited literature [23 references]  Display  Hide  Download

https://hal.inria.fr/hal-01540760
Contributor : Guillaume Munch-Maccagnoni <>
Submitted on : Friday, June 16, 2017 - 3:10:02 PM
Last modification on : Tuesday, March 26, 2019 - 9:25:22 AM
Long-term archiving on : Wednesday, December 13, 2017 - 1:40:27 PM

File

ll-cbpv.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01540760, version 1

Citation

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

Share

Metrics

Record views

350

Files downloads

119