F.Honsell, M. Lenisa, and R. Redamalla. Strict geometry of interaction graph models. In Proceedings of LPAR'03, volume 2850 of Lecture Notes in Artificial Intelligence, pages 403-417. Springer Verlag, 2003.

We study a class of ``wave-style'' Geometry of Interaction (GoI) lambda-models based on the category Rel of sets and relations. Wave GoI models arise when Abramsky's GoI axiomatization, which generalizes Girard's original GoI, is applied to a traced monoidal category with the categorical product as tensor, using ``countable power'' as the traced strong monoidal functor bang. Abramsky hinted that the category Rel is the basic setting for traditional denotational ``static semantics''. However, Rel, together with the cartesian product, apparently escapes Abramsky's original GoI construction. Here we show that Rel can be axiomatized as a strict GoI situation, i.e. a strict variant of Abramsky's GoI situation, which gives rise to a rich class of strict graph models. These are models of restricted lambda-calculi in the sense of [HL99], such as Church's lambda-I-calculus and the lambda-beta-KN-calculus.

[ bib | http ]

Back