Parametric Chu Translation

EasyChair Preprint 8624

Abstract

Bellin translates multiplicative-additive linear logic to its intuitionistic fragment by relating the Chu construction to trips on a proof net, seemingly posing an alternative to negative translation. However, his translation is not sound in the sense that not all valid intuitionistic sequents in its image correspond to valid classical ones. By directly analyzing two-sided classical sequents, we develop a sound generalization thereof inspired by parametric negative translation that also handles the exponentials.

Keyphrases: Chu construction, negative translation, proof theory

@booklet{EasyChair:8624,
  author    = {Siva Somayyajula},
  title     = {Parametric Chu Translation},
  howpublished = {EasyChair Preprint 8624},
  year      = {EasyChair, 2022}}