# Is there a "lambda cube" for interaction nets?

The lambda calculus is an untyped language that is often extended with logical frameworks such as the vertices of the λ-cube. Is there something similar to it, but for interaction nets? What about interaction combinators?

• I doubt it. There is not much research on interaction nets. It should be possible to look at it all. Feb 4, 2016 at 11:24

The Structure of Interaction paper seems to be what you are asking for.

• Maybe, but I'm not so sure I make the connection between what is presented on this paper and my understanding of the λ-cube and dependent types. For example, how'd you express dependent types, things like the λ (t : *) -> λ (x : t) -> x term (Morte syntax)? Sep 22, 2017 at 23:58

Like Martin said, nothing like an equivalent for the $\lambda$-cube has ever been developed for interaction nets or interaction combinators.

The only work that considers types for interaction nets is Lafont's original paper [1]. (My own CONCUR 2005 paper also considers types but adds nothing new to what Lafont did). It is an extremely simple system: only basic types plus a polarity, no type constructors at all. Nevertheless, it is enough to obtain a desirable safety property: a well typed net cannot reduce to a net containing a "clash" (an active pair which does not have a corresponding reduction rule and is therefore "stuck").

Of course, since multiplicative linear logic proof nets are a particular system of interaction nets, it is defintely possible to equip certain systems of interaction nets with more complex types, using non-trivial type constructors. But nothing has ever been studied, mostly because the interest of such an endevour is unclear.

[1] Yves Lafont, Interaction Nets. In Proceedings of POPL, 1990.

• One more thing: this year at POPL, Stéphane Gimenez and Georg Moser had a paper using interaction nets (for studying complexity properties). I missed their talk and haven't yet seen the paper, but it's possible that it contains some new work on types for interaction nets, although I doubt it is anything in the style of the $\lambda$-cube types. Feb 4, 2016 at 12:17
• So my question is more in the lines - interaction nets aren't as useful for proofs and related as the λ-calculus, I guess? Feb 4, 2016 at 12:26
• @DamianoMazza Lafont's POPL paper is available electronically here and, if you can access the ACM library, here. Feb 5, 2016 at 8:37
• @MartinBerger That's great, thank you! The last time I checked there was no electronic copy freely available, but it was a long time ago, somebody must have scanned it in the meantime! Feb 5, 2016 at 10:01