<p><a href="http://cl-informatik.uibk.ac.at/users/sgimenez/data/articles/soi.pdf" rel="nofollow noreferrer">The Structure of Interaction</a> paper seems to be what you are asking for.</p>

CC BY-SA 3.0
2017-09-22T23:58:57.580Z
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)?
MaiaVictor
CC BY-SA 4.0
2017-09-22T23:29:49.077Z
2018-05-18T15:30:12.423Z
2018-05-18T15:30:12.423Z
Łukasz Lew
<p>Like Martin said, nothing like an equivalent for the $\lambda$-cube has ever been developed for interaction nets or interaction combinators.</p>

<p>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").</p>

<p>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.</p>

<p>[1] Yves Lafont, Interaction Nets.  In <em>Proceedings of POPL</em>, 1990.</p>

CC BY-SA 3.0
2016-02-04T12:17:57.900Z
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.
Damiano Mazza
CC BY-SA 3.0
2016-02-04T12:26:02.773Z
So my question is more in the lines - interaction nets aren't as useful for proofs and related as the λ-calculus, I guess?
MaiaVictor
CC BY-SA 3.0
2016-02-05T08:37:03.857Z
@DamianoMazza Lafont's POPL paper is available electronically [here](http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.112.2822&rep=rep1&type=pdf) and, if you can access the ACM library, [here](https://dl.acm.org/citation.cfm?id=96718).
Martin Berger
CC BY-SA 3.0
2016-02-05T10:01:16.983Z
@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!
Damiano Mazza
CC BY-SA 3.0
2016-02-04T12:14:04.140Z
2016-02-04T12:14:04.140Z
Damiano Mazza
<p>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?</p>

CC BY-SA 3.0
2016-02-04T11:24:43.610Z
I doubt it. There is not much research on interaction nets. It should be possible to look at it all.
Martin Berger
<type-theory><lambda-calculus><type-systems><interaction-nets>
Is there a "lambda cube" for interaction nets?
MaiaVictor
# Is there a "lambda cube" for interaction nets?

(Asked by: username_0 on 2016-02-04)

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?

**Tags:** type-theory, lambda-calculus, type-systems, interaction-nets
> **Comments:**
> **username_1**: I doubt it. There is not much research on interaction nets. It should be possible to look at it all.  

---

## 2 answers

### Answer by username_2 on 2017-09-22. Score: 1 | Accepted answer

[The Structure of Interaction](http://cl-informatik.uibk.ac.at/users/sgimenez/data/articles/soi.pdf) paper seems to be what you are asking for.

> **Comments:**
> **username_0**: 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)?  

---

### Answer by username_3 on 2016-02-04. Score: 4

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.

> **Comments:**
> **username_3**: 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.  
> **username_0**: So my question is more in the lines - interaction nets aren't as useful for proofs and related as the λ-calculus, I guess?  
> **username_1**: @DamianoMazza Lafont's POPL paper is available electronically [here](http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.112.2822&rep=rep1&type=pdf) and, if you can access the ACM library, [here](https://dl.acm.org/citation.cfm?id=96718).  
> **username_3**: @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!  

---

