Note on models of polarised intuitionistic logic

Guillaume Munch-Maccagnoni 1
1 GALLINETTE - GALLINETTE
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.
Type de document :
Pré-publication, Document de travail
2017
Liste complète des métadonnées


https://hal.inria.fr/hal-01540760
Contributeur : Guillaume Munch-Maccagnoni <>
Soumis le : vendredi 16 juin 2017 - 15:10:02
Dernière modification le : samedi 17 juin 2017 - 01:20:44

Fichier

ll-cbpv.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01540760, version 1

Collections

Citation

Guillaume Munch-Maccagnoni. Note on models of polarised intuitionistic logic. 2017. <hal-01540760>

Partager

Métriques

Consultations de
la notice

101

Téléchargements du document

33