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

Guillaume Munch-Maccagnoni 1
1 GALLINETTE - GALLINETTE
Inria Rennes – Bretagne Atlantique , LS2N - Laboratoire des Sciences du Numérique de Nantes
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 : dimanche 10 septembre 2017 - 23:38:45
Dernière modification le : mardi 12 septembre 2017 - 01:08:28

Fichier

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

Identifiants

  • HAL Id : hal-01528857, version 3

Collections

Citation

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

Partager

Métriques

Consultations de
la notice

48

Téléchargements du document

9