Skip to Main content Skip to Navigation
Preprints, Working Papers, ...

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

Guillaume Munch-Maccagnoni 1, 2
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 metadata

Cited literature [29 references]  Display  Hide  Download
Contributor : Guillaume Munch-Maccagnoni Connect in order to contact the contributor
Submitted on : Sunday, September 10, 2017 - 11:38:45 PM
Last modification on : Friday, January 21, 2022 - 3:09:58 AM


Files produced by the author(s)


  • HAL Id : hal-01528857, version 3


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



Les métriques sont temporairement indisponibles