A journey through resource control lambda calculi and explicit substitution using intersection types (an account)

Abstract : In this paper we invite the reader to a journey through three lambda calculi with resource control: the lambda calculus, the sequent lambda calculus, and the lambda calculus with explicit substitution. All three calculi enable explicit control of resources due to the presence of weakening and contraction operators. Along this journey, we propose intersection type assignment systems for all three resource control calculi. We recognise the need for three kinds of variables all requiring different kinds of intersection types. Our main contribution is the characterisation of strong normalisation of reductions in all three calculi, using the techniques of reducibility, head subject expansion, a combination of well-orders and suitable embeddings of terms.
Type de document :
Rapport
2011, pp.40
Liste complète des métadonnées

Littérature citée [60 références]  Voir  Masquer  Télécharger

https://hal-ens-lyon.archives-ouvertes.fr/ensl-00823621
Contributeur : Pierre Lescanne <>
Soumis le : lundi 10 juin 2013 - 17:23:50
Dernière modification le : mardi 24 avril 2018 - 13:52:39
Document(s) archivé(s) le : mercredi 11 septembre 2013 - 04:14:46

Fichiers

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

Identifiants

  • HAL Id : ensl-00823621, version 2
  • ARXIV : 1306.2283

Collections

Citation

Silvia Ghilezan, Jelena Ivetic, Pierre Lescanne, Silvia Likavec. A journey through resource control lambda calculi and explicit substitution using intersection types (an account). 2011, pp.40. 〈ensl-00823621v2〉

Partager

Métriques

Consultations de la notice

294

Téléchargements de fichiers

74