Skip to Main content Skip to Navigation
Preprints, Working Papers, ...

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.
Document type :
Preprints, Working Papers, ...
Complete list of metadata
Contributor : Pierre Lescanne Connect in order to contact the contributor
Submitted on : Saturday, December 6, 2014 - 10:23:40 AM
Last modification on : Saturday, September 11, 2021 - 3:18:20 AM
Long-term archiving on: : Monday, March 9, 2015 - 6:07:02 AM


Files produced by the author(s)


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



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



Les métriques sont temporairement indisponibles