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.

Domains

Computer Science [cs] Logic in Computer Science [cs.LO] Computer Science [cs] Programming Languages [cs.PL]
Fichier principal
Vignette du fichier
curry.pdf (497.69 Ko) Télécharger le fichier
Origin : Files produced by the author(s)

Guillaume Munch-Maccagnoni  : Connect in order to contact the contributor

https://hal.inria.fr/hal-01528857

Submitted on : Sunday, September 10, 2017-11:38:45 PM

Last modification on : Thursday, December 1, 2022-11:00:07 AM

Download

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⟩

Export

BibTeX TEI Dublin Core DC Terms EndNote Datacite

Collections

UNIV-NANTES INSTITUT-TELECOM CNRS INRIA EC-NANTES UNAM INRIA2 LS2N LS2N-GALLINETTE NANTES-UNIVERSITE
625 View
331 Download

Share

Gmail Facebook Twitter LinkedIn More