A Correspondence between Maximal Abelian Sub-Algebras and Linear Logic Fragments
Logic
2016-08-03 v2 Logic in Computer Science
Abstract
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.
Keywords
Cite
@article{arxiv.1408.2125,
title = {A Correspondence between Maximal Abelian Sub-Algebras and Linear Logic Fragments},
author = {Thomas Seiller},
journal= {arXiv preprint arXiv:1408.2125},
year = {2016}
}