Service interruption on Monday 11 July from 12:30 to 13:00: all the sites of the CCSD (HAL, EpiSciences, SciencesConf, AureHAL) will be inaccessible (network hardware connection).
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 : Monday, February 7, 2022 - 4:06:03 PM
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⟩



Record views


Files downloads