Skip to Main content Skip to Navigation
Preprints, Working Papers, ...

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 metadata

Cited literature [23 references]  Display  Hide  Download
Contributor : Guillaume Munch-Maccagnoni Connect in order to contact the contributor
Submitted on : Friday, June 16, 2017 - 3:10:02 PM
Last modification on : Friday, January 21, 2022 - 3:09:59 AM
Long-term archiving on: : Wednesday, December 13, 2017 - 1:40:27 PM


Files produced by the author(s)


  • HAL Id : hal-01540760, version 1


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



Les métriques sont temporairement indisponibles