How Linear is Howe?

In recent years there has been much progress in the use of operationally based methods for reasoning about programs. Notions such as contextual equivalence and bisimilarity, which are historically more usually associated with functional programming and concurrency respectively, have been shown to be very closely connected, and such connections can be seen throughout the functional, concurrent and indeed imperative paradigms. In this paper we show that operational techniques from these three settings also apply in a linear functional setting, by proving that in a simple linear type theory involving function types and tensor types, one can establish linear contextual equivalences by coinductive techniques