×

zbMATH — the first resource for mathematics

New foundations for the geometry of interaction. (English) Zbl 0803.03014
J.-Y. Girard defined interpretation of (derivations in) linear logic in \(C^*\)-algebras. This allowed him to write an explicit formula for cut- elimination which works for a subsystem. The authors propose an alternative categorical interpretation based on elementary domain theory, which works for the whole second-order linear logic. Girard’s formula is replaced by a least fixed-point.
Reviewer: G.Mints (Stanford)

MSC:
03B70 Logic in computer science
68Q55 Semantics in the theory of computing
PDF BibTeX XML Cite
Full Text: DOI