# 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
Full Text: