Note on Curry's style for Linear Call-by-Push-Value

Guillaume Munch-Maccagnoni 1
1 GALLINETTE - GALLINETTE
Inria Rennes – Bretagne Atlantique
Abstract : We present Curry-style calculi for intuitionistic (linear) logic with polarised evaluation order and give self-contained proofs of their main properties and of their interpretation into (Linear) Call-by-Push-Value models: subject reduction, confluence, strong normalisation, coherence, soundness, and focusing.
Type de document :
Pré-publication, Document de travail
2017
Liste complète des métadonnées


https://hal.inria.fr/hal-01528857
Contributeur : Guillaume Munch-Maccagnoni <>
Soumis le : lundi 29 mai 2017 - 21:17:54
Dernière modification le : samedi 17 juin 2017 - 01:20:44

Fichier

curry.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01528857, version 1

Collections

Citation

Guillaume Munch-Maccagnoni. Note on Curry's style for Linear Call-by-Push-Value. 2017. <hal-01528857>

Partager

Métriques

Consultations de
la notice

50

Téléchargements du document

27