We introduce a linear infinitary -calculus, called ℓ, 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 ℓΔ, 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 ℓ built around the principles of SLL and 4LL. Interestingly, it enjoys confluence, contrarily to what happens in ordinary infinitary -calculi.

Infinitary Lambda Calculi from a Linear Perspective

DAL LAGO, UGO
2016

Abstract

We introduce a linear infinitary -calculus, called ℓ, 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 ℓΔ, 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 ℓ built around the principles of SLL and 4LL. Interestingly, it enjoys confluence, contrarily to what happens in ordinary infinitary -calculi.
2016
Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science
447
456
Dal Lago, Ugo
File in questo prodotto:
Eventuali allegati, non sono esposti

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11585/585943
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 1
  • ???jsp.display-item.citation.isi??? 1
social impact