Intersection Types for the Resource Control Lambda Calculi

Pierre Lescanne 1 Silvia Ghilezan 2 Jelena Ivetic 2 Silvia Likavec 3
1 LIP - Laboratoire de l'Informatique du Parallélisme
2 Faculty of engineering, University of Novi Sad
3 Dipartimento di Informatica [Torino]
Abstract : 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.
Mots-clés : lambda calculus sequent calculus resource control intersection types strong normalisation
Type de document :
Communication dans un congrès
Antonio Cerone et Pekka Pihlajasaari. Theoretical Aspects of Computing - ICTAC 2011 - 8th International Colloquium, Aug 2011, Johannesburg, South Africa. Springer, 6916, pp.116-134, 2011, Lecture Notes in Computer Science
Liste complète des métadonnées
https://hal-ens-lyon.archives-ouvertes.fr/ensl-00654755
Contributeur : Pierre Lescanne <>
Soumis le : jeudi 22 décembre 2011 - 20:28:12
Dernière modification le : mardi 24 avril 2018 - 13:52:22

Identifiants

  • HAL Id : ensl-00654755, version 1

Collections

ENS-LYON | INRIA | LIP | INSMI | UNIV-LYON1

Citation

Pierre Lescanne, Silvia Ghilezan, Jelena Ivetic, Silvia Likavec. Intersection Types for the Resource Control Lambda Calculi. Antonio Cerone et Pekka Pihlajasaari. Theoretical Aspects of Computing - ICTAC 2011 - 8th International Colloquium, Aug 2011, Johannesburg, South Africa. Springer, 6916, pp.116-134, 2011, Lecture Notes in Computer Science. 〈ensl-00654755〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

101

Contact

support.ccsd.cnrs.fr
hal.support@ccsd.cnrs.fr
Logo CCSD