A Correspondence between Maximal Abelian Sub-Algebras and Linear Logic Fragments

Understand

We show a correspondence between a classification of maximal abelian sub-algebras (MASAs) proposed by Jacques Dixmier and fragments of linear logic.

• We expose for this purpose a modified construction of Girard's hyperfinite geometry of interaction which interprets proofs as operators in a von Neumann algebra.
• The expressivity of the logic soundly interpreted in this model is dependent on properties of a MASA which is a parameter of the interpretation.
• We also unveil the essential role played by MASAs in previous geometry of interaction constructions.