Dialectica Interpretation - Dialectica Interpretation of Linear Logic

Dialectica Interpretation of Linear Logic

The Dialectica interpretation has been used to build a model of Girard's refinement of intuitionistic logic known as linear logic, via the so-called Dialectica spaces. Since linear logic is a refinement of intuitionistic logic, the dialectica interpretation of linear logic can also be viewed as a refinement of the dialectica interpretation of intuitionistic logic.

Although the linear interpretation in validates the weakening rule (it is actually an interpretation of affine logic), the dialectica spaces interpretation does not validate weakening for arbitrary formulas.