Note on Curry's style for Linear Call-by-Push-Value - Archive ouverte HAL Access content directly
Preprints, Working Papers, ... Year :

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

(1, 2)
1
2

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.
Fichier principal
Vignette du fichier
curry.pdf (497.69 Ko) Télécharger le fichier
Origin : Files produced by the author(s)
Loading...

Dates and versions

hal-01528857 , version 1 (29-05-2017)
hal-01528857 , version 2 (31-08-2017)
hal-01528857 , version 3 (10-09-2017)

Identifiers

  • HAL Id : hal-01528857 , version 3

Cite

Guillaume Munch-Maccagnoni. Note on Curry's style for Linear Call-by-Push-Value. 2017. ⟨hal-01528857v3⟩
625 View
331 Download

Share

Gmail Facebook Twitter LinkedIn More