Note on Curry's style for Linear Call-by-Push-Value
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.
Origin : Files produced by the author(s)
Loading...