Resource control and intersection types: an intrinsic connection

Abstract : In this paper we investigate the λ -calculus, a λ-calculus enriched with resource control. Explicit control of resources is enabled by the presence of erasure and duplication operators, which correspond to thinning and con-traction rules in the type assignment system. We introduce directly the class of λ -terms and we provide a new treatment of substitution by its decompo-sition into atomic steps. We propose an intersection type assignment system for λ -calculus which makes a clear correspondence between three roles of variables and three kinds of intersection types. Finally, we provide the characterisation of strong normalisation in λ -calculus by means of an in-tersection type assignment system. This process uses typeability of normal forms, redex subject expansion and reducibility method.
Type de document :
Pré-publication, Document de travail
2014
Liste complète des métadonnées

https://hal-ens-lyon.archives-ouvertes.fr/ensl-01091753
Contributeur : Pierre Lescanne <>
Soumis le : samedi 6 décembre 2014 - 10:23:40
Dernière modification le : mardi 24 avril 2018 - 13:52:53
Document(s) archivé(s) le : lundi 9 mars 2015 - 06:07:02

Fichiers

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

Identifiants

  • HAL Id : ensl-01091753, version 1
  • ARXIV : 1412.2219

Collections

Citation

S Ghilezan, J Ivetic, P Lescanne, S Likavec. Resource control and intersection types: an intrinsic connection. 2014. 〈ensl-01091753〉

Partager

Métriques

Consultations de la notice

104

Téléchargements de fichiers

50