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

Guillaume Munch-Maccagnoni 1
1 GALLINETTE - Gallinette : vers une nouvelle génération d'assistant à la preuve
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.
Complete list of metadatas

Cited literature [26 references]  Display  Hide  Download

https://hal.inria.fr/hal-01528857
Contributor : Guillaume Munch-Maccagnoni <>
Submitted on : Thursday, August 31, 2017 - 7:12:22 PM
Last modification on : Tuesday, March 26, 2019 - 9:25:22 AM
Long-term archiving on : Friday, December 1, 2017 - 7:38:15 PM

File

curry.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01528857, version 2

Citation

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

Share

Metrics

Record views

30

Files downloads

53