Authors: Ghilezan, Silvia 
Ivetić, Jelena
Lescanne, Pierre
Likavec, Silvia
Title: Intersection types for the resource control lambda calculi
Journal: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume: 6916 LNCS
First page: 116
Last page: 134
Conference: 8th International Colloquium on Theoretical Aspects of Computing, ICTAC 2011; Johannesburg; South Africa; 31 August 2011 through 2 September 2011
Issue Date: 19-Sep-2011
Rank: M33
ISBN: 978-3-642-23282-4
ISSN: 0302-9743
DOI: 10.1007/978-3-642-23283-1_10
We propose intersection type assignment systems for two resource control term calculi: the lambda calculus and the sequent lambda calculus with explicit operators for weakening and contraction. These resource control calculi, λ® and λ®Gtz, respectively, capture the computational content of intuitionistic natural deduction and intuitionistic sequent logic with explicit structural rules. Our main contribution is the characterisation of strong normalisation of reductions in both calculi. We first prove that typability implies strong normalisation in λ® by adapting the reducibility method. Then we prove that typability implies strong normalisation in λ®Gtz by using a combination of well-orders and a suitable embedding of λ®Gtz-terms into λ®-terms which preserves types and enables the simulation of all its reductions by the operational semantics of the λ®-calculus. Finally, we prove that strong normalisation implies typability in both systems using head subject expansion.
Publisher: Springer Link

Show full item record


checked on Jun 15, 2024

Page view(s)

checked on May 9, 2024

Google ScholarTM




Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.