Infinitary Lambda Calculi from a Linear Perspective

Ugo Dal Lago 1, 2
2 FOCUS - Foundations of Component-based Ubiquitous Systems
CRISAM - Inria Sophia Antipolis - Méditerranée , DISI - Dipartimento di Informatica - Scienza e Ingegneria [Bologna]
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 applica-tive λ-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 coin-ductively. 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.
Type de document :
Communication dans un congrès
Logic in Computer Science, Jul 2016, New York, United States. 〈10.1145/2933575.2934505〉
Liste complète des métadonnées

Littérature citée [30 références]  Voir  Masquer  Télécharger
Contributeur : Ugo Dal Lago <>
Soumis le : mardi 22 novembre 2016 - 16:02:44
Dernière modification le : mercredi 10 octobre 2018 - 10:09:13
Document(s) archivé(s) le : lundi 27 mars 2017 - 09:19:44


main (1).pdf
Fichiers produits par l'(les) auteur(s)




Ugo Dal Lago. Infinitary Lambda Calculi from a Linear Perspective. Logic in Computer Science, Jul 2016, New York, United States. 〈10.1145/2933575.2934505〉. 〈hal-01400883〉



Consultations de la notice


Téléchargements de fichiers