Paper detail

Infinitary $λ$-Calculi from a Linear Perspective (Long Version)

We introduce a linear infinitary $λ$-calculus, called $\ellΛ_{\infty}$, in which two exponential modalities are available, the first one being the usual, finitary one, the other being the only construct interpreted coinductively. The obtained calculus embeds the infinitary applicative $λ$-calculus and is universal for computations over infinite strings. What is particularly interesting about $\ellΛ_{\infty}$, is that the refinement induced by linear logic allows to restrict both modalities so as to get calculi which are terminating inductively and productive coinductively. We exemplify this idea by analysing a fragment of $\ellΛ$ built around the principles of $\mathsf{SLL}$ and $\mathsf{4LL}$. Interestingly, it enjoys confluence, contrarily to what happens in ordinary infinitary $λ$-calculi.