On Various Translations Between Classical, Intuitionistic, and Linear Logic

Ferreira, G., Oliva, P. & Protin, C.L. On Various Translations Between Classical, Intuitionistic, and Linear Logic. Stud Logica (2026). https://doi.org/10.1007/s11225-026-10251-y

Several different proof translations exist between classical and intuitionistic logic (negative translations), and intuitionistic and linear logic (Girard translations). Our aims in this paper are: (1) to consider extensions of intuitionistic linear logic corresponding to each of these systems, and (2) using this common logical basis, to develop a uniform approach to devising and simplifying proof translations. Through this process of “simplification” we recover most of the well-known translations in the literature.